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?
Maybe (for humans the two often go together), but what's the hypothesis behind assuming it will do the one and not the other? It seems like a very specific and arbitrary bet, not much unlike betting that AI will be able to learn English but not French.
I'm probably being naive here, but with theorem proving, if you have a problem then you can check whether a given solution is correct, letting people make things like AlphaProof, no? I would think that the open-endedness of software development in general would complicate that.
In general, problems whose solutions are easily checkable are not necessarily easily solvable, and the difficulty of finding the proof also depends on how the software is written, which is why humans, at least, don't try to prove arbitrary programs correct, but write the program and the proof together. But regardless, the tools involved are really not very complicated. While it's possible, I find it hard to justify betting on AI being able to prove a 100KLOC-10MLOC program correct while not being able to write a 10KLOC tool well enough.
pron · · focus · HN ↗
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?
creata · · focus · HN ↗
Doesn't it only need to become an order of magnitude more capable than humans at theorem proving, not general software development?
pron · · focus · HN ↗
creata · · focus · HN ↗
pron · · focus · HN ↗