$\bot \vdash \top$

- A favorite proof of mine 06 March 2023

There are a lot of proofs in mathematics. Many of them serve to verify what we intuitively know to be true, some of them shed light on new methods, and some reveal new ways to view old ideas. Some proofs leave us with a headache, some leave us bored, and some leave us with wonder. In this blog post I will share a beautiful proof leading to a closed formula for the $n$-th Fibonacci number, taking us on a detour into functional programming and linear algebra.

- Haskell and Logic 15 December 2022

Haskell programs are proofs, don’t you know? Hidden inside the types of Haskell lies a deep connection to mathematical logic. Given some basic Haskell knowledge and mathematical interest, you too may experience the sense of wonder I first did when discovering the Curry-Howard isomorphism.

- Why be pure? 10 December 2022

Newcomers to Haskell are often told that Haskell is “pure”, or that it is “mathematical”. It is often not clear what this means, or why these properties would be of interest to begin with. In this blog post I aim to combat this by showing why purity can be helpful, both in writing programs and improving performance.

- A look at SECD machines 10 December 2021

The SECD machine is a virtual machine designed to evaluate lambda expressions. It’s purpose is to be a more natural goal for compilers than assembly while maintaining reasonable execution speed. In this blog post I will give you a quick intro to SECD machines and an overview of a simple implementation.

- Running Linux on the Thinkpad X13 Yoga (Gen 2) 09 October 2021

This is a rather short blog post on how to get the Thinkpad X13 Yoga (Gen 2) working properly on Linux. This includes, making audio work, removing screen tears, making the screen auto rotate, and making the desktop a comfortable size.

- Writing portable Makefiles 22 January 2021

Makefiles are a great portable tool for compiling your programs which any POSIX compliant system will provide, however, a lot of Makefiles are GNU Makefiles, which are less portable. This blog post will not only explain how to write Makefiles, but how to emulate GNU make features.