Blog
Formal methods can start small
Proof assistants are introduced through their hardest applications, so people assume opening one means a large project. A four-state Agda specification, compiled and used as the test oracle for Go code, shows how small the useful unit has become, and what formalizing Yovico's payment rules turned up.
How I Learned to Stop Worrying and Tell the AI What I Mean
My first program ran on an IBM 370, three runs a day, and after a few months I could read every line and not recover the thought that arranged them. AI agents put us back in that spot from the other side: the code arrives fast, and the intention still lives nowhere. At Yovico the intention lives in Agda, compiled into an oracle that argues back.
If you look into an LLM long enough, it starts looking back at you
Sycophancy is not a manners problem. It is the mirror aimed at you. A room of personas that argue with each other breaks the mirror, and the expensive reasoning model is the wrong one to put in it.
The Mythical Prototype
Building a prototype is easy now. Open source made it easy, AI made it easier. Building a product is not, and never was. The cost was never in the code. It is in the interactions, the parts that have to agree with each other, and the rework you never see coming until real users hit the thing. Brooks explained this in 1975. None of it has changed.
Email metamorphosed
I spent a week trying to get permission to email my own users. Email is not a communication medium anymore. It is an identity service wearing a mailbox.
Experience Got Cheap. Talent Didn't.
When the LLMs got good, most large companies fired the juniors. AI is a great assistant, seniors have judgment, juniors were the assistants, ergo juniors are redundant. Half of tech wrote the same memo. I did the opposite, and bet on smarts and conscientiousness instead.
The Best Patent I Never Filed
2FA is not, primarily, a security feature. It's an account-sharing prevention feature wearing a security costume - and the reason 'send the code to a pager' failed in 2000 has nothing to do with security.
The OWASP ZAP scan that wasn't going to happen
Last year, an intern needed two weeks to set up OWASP ZAP scans. This week I set it up for Yovico in an hour - and Claude Code filed the issues, updated the docs, rewrote the security attestation, and turned the whole thing into a slash command.
The Inference Tax
How AI vendor pricing is structured to extract from the developers it claims to empower - and what that means for founders building outside the moat.
Exploratory Testing Got Cheap
For two decades the trajectory of QA was toward verification and away from exploration, for sound economic reasons. Those reasons just stopped applying. We sent an AI agent to explore our AI agent platform unattended, with no test plan. It found things we never would have written tests for.
The Unbureaucratic Company
For twenty-five years, the startup industry ran a quiet experiment: what happens when technology stops being hard? The answer turned out to be middle management. AI is ending that experiment.
From Simulacron to Simulation Engine
The idea of using artificial minds to simulate business situations didn't start with LLMs. It started with a 1964 science fiction novel, a Soviet mathematician who nearly built the internet, and a generation of writers who understood distributed cognition before the engineers did.