Formal verification doesn’t eliminate risk. It relocates it into the spec, the model, and the trusted base. Five runnable Lean 4 proofs that compile cleanly and still sit on real bugs.

On pain, building, capitalism, discipline, and realizing I had treated love as something that came after the work.

LLM APIs ask you to trust that the provider ran the model and settings they advertise. CommitLLM adds cryptographic receipts and audits without zero-knowledge prover costs.

Turing completeness is a shallow pit you fall into. Self-replication is an even shallower one. A recent paper shows that self-replicating programs spontaneously emerge from soups of random code, no design required.

An ordered, evidence-based health guide for nerds who used to think the body didn’t matter.

What happens to the West’s services advantage when strong AI models are free, portable, and running on every laptop?

Our stack and practices for building SaaS applications: Elixir on the backend, React on the frontend, Nix for everything else. No Docker. No Kubernetes.

A practical guide to type systems, from everyday generics to dependent types that prove correctness, with examples in Rust, Scala, and Idris

Crypto found product-market fit where trust is weakest: inflationary or censored economies, and internet-native communities that need programmable coordination and markets.

The proving-verification asymmetry in zero-knowledge proofs is what makes them economically meaningful: proving is expensive, verification is cheap, and that gap changes what systems can be built without trust.