Fits on a Floppy. Shipping software that people use also means that you should be strict about what you put on people’s computers. It’s akin to being a guest in someone’s house; you want to be polite to your host(s). Keeping binary sizes small is one of the ways to be a good guest.

“Why not just use Lean?”. A post pushing back on using Lean as the default for formal verification everywhere. In some applications, having dependent types is overkill. Higher Order Logic (HOL) can do the job. Sequent’s article talks more in-depth on why HOL is good enough for deep verification.

A Font That is a Neural Network. Cool experiment on how you can replace the lookup that renders an OpenType font with a computation.

Godel’s Proof by Ernest Nagel & James Newman. Picked up this book in a bookstore in Prague. Explains Godel’s Incompleteness Theorem by building up the required background knowledge, and does it concisely.

Roger Penrose explains Godel’ s Incompleteness Theorem. A 3 minute watch.

Slow Software: The Case for High latency Systems Development. A bit corny with the slow food analogy but somewhat aligns with my belief. Generating code is no longer the bottleneck, reading and understanding is. Slower and more deliberate cycles allow for more resilient and secure systems.