I love TLA+ to describe systems precisely yet succinctly and reason about them. But as someone who's been using formal methods to help software development for many years, this whole industry around tools to connect such a wonderful mathematical language and others like it, like Lean, with AI, to the point of hiding the reasoning from people, confuses me.
Proving programs correct end-to-end (i.e. code to high-level properties) - as this company and others purport to do - is so difficult that humans have only been able to do it for very small programs (~10KLOC) and even then, in very specialised cases, where the programs have been written in an extra-simple way (often at the cost of performance, because performance often requires more complicated algorithms). If AI becomes at least an order of magnitude more capable than humans at software development, which is what will be required for this task, would it need our help to write various tools and harnesses that help with the task? After all, writing these tools is so much easier than using them for that goal that I don't understand the hypothesis behind AI capability here.
This company says: they're "developing the agentic frameworks to make these correctness guarantees accessible to all software engineers". But developing all that is the easy part! If AI can do the hard part, why does it need our help to make this accessible, it can surely find a way to do that easy part itself! It's like saying, "Soon we'll have a machine that can harness so much energy to boil an ocean; we've built a service that lets you order a taxi to take the machine to the beach!"
Why would an AI that is so much better than us at writing software need our help writing any kind of software for it?
Proving programs correct end-to-end (i.e. code to high-level properties) - as this company and others purport to do - is so difficult that humans have only been able to do it for very small programs (~10KLOC) and even then, in very specialised cases, where the programs have been written in an extra-simple way (often at the cost of performance, because performance often requires more complicated algorithms). If AI becomes at least an order of magnitude more capable than humans at software development, which is what will be required for this task, would it need our help to write various tools and harnesses that help with the task? After all, writing these tools is so much easier than using them for that goal that I don't understand the hypothesis behind AI capability here.
This company says: they're "developing the agentic frameworks to make these correctness guarantees accessible to all software engineers". But developing all that is the easy part! If AI can do the hard part, why does it need our help to make this accessible, it can surely find a way to do that easy part itself! It's like saying, "Soon we'll have a machine that can harness so much energy to boil an ocean; we've built a service that lets you order a taxi to take the machine to the beach!" Why would an AI that is so much better than us at writing software need our help writing any kind of software for it?