There has been a lot of talk about formalizing mathematics recently, ever since OpenAI proposed a solution to the famous Navier-Stokes problem formalized in Lean. Since I did some work in mathematical logic in the past, I thought it might be useful to clarify what the talk is all about... Read more.

People tend to say that AI is bringing programming to a higher layer of abstraction: the human language. However, there's a big elephant in the room. Any human language is vague. I argue here that the next layer of abstraction might as well be formal specifications grounded in logic. We can build apps around specifications and let AI agents generate code that satisfy our specifications. Our specifications also determine what kinds of decisions about code we delegate to the agents. This is why specification-driven development is more relevant now than ever. .. Read more.

I'm far from being a coffee expert, but I started getting into coffee a bit and thought I could use a summary of what I came to learn... Read more.

We don’t want bugs in our code, period. Bugs are not only annoying, they can cost us millions of dollars if they go unnoticed. No matter how hard we try, every time we remove a bug, another pops up in a seemingly unrelated part of the code base... Read more.

I never believed I would be writing this. Don't get me wrong. I love both Haskell and Hakyll, which builds upon using one of the strongest conversion tools for markup the world has known: Pandoc. Needless to say that this very blog runs on Hakyll. However, nothing can advance without somebody laying out loud the things that don't work. And with Hakyll it seems like such a list is long overdue... Read more.