Brief writeup on how to utilize the Curry-Howard correspondence to check natural deduction proofs encoded in Haskell at compile-time. ( ´ ▽ ` )ﾉ

The Game Boy Camera is such an interesting piece of technology. That’s why it breaks my heart to announce that my unit is DEAD.. sort of. (´；ω；`)

Sequent is a Fitch-style first-order logic proof language and web app for checking, formatting, and rendering proofs with clickable diagnostics.

A quick showcase of my OLKB Planck Rev. 7, along with the switches and keycaps I’ve equipped it with.

A tour through the compact QMK keyboard layout I use across my Planck, Corne, and Ergodox, including the reasoning behind this specific arrangement.