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.