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?
I have long being fascinated by the the field and curious about it on an amature level, i took some basic proof verification and distributed computing classes back in the grad school days, but I'm clearly not an expert in the field by any means. From the article, it seemed like there are plenty of "traps" that i did not even consider - starting from lean hatches like assume(false), expressive power of TLA+ (CTL, ATL), and ofc challenges of tying an real implementation to a proof. To me all three of the above seem challenging enough to deserve their own tools, and i would appreciate smart people putting effort into addressing these rough edges.
Question to you: i can understand how proof verification like z3 or lean requires a special language and an inference engine; given that model checkers like tla+ are mostly about exploring possible program states and checking properties of such states and chains of states, i do not quite understand why it can't be done with a conventional imperative language to express state transitions and invariants - especially an interpreted one like python (esp with continuation support) or a language targeting a vm like wasm where one should be able to snapshot program state?
The state space you get when using real programming languages like Python is much, much larger than the one you get when abstracting your system design into TLA+. Thus when testing real systems you can only explore very small portions of the state space. This is a real thing people do, although it isn't yet widespread - the term to look for is deterministic simulation testing. Making a DST harness that can handle exploring an application state space without requiring large modification to the application itself is very challenging. Currently Antithesis are the only ones I know who have done it (disclaimer: no connection to this company, I just think they are very cool).
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?
bbminner · · focus · HN ↗
Question to you: i can understand how proof verification like z3 or lean requires a special language and an inference engine; given that model checkers like tla+ are mostly about exploring possible program states and checking properties of such states and chains of states, i do not quite understand why it can't be done with a conventional imperative language to express state transitions and invariants - especially an interpreted one like python (esp with continuation support) or a language targeting a vm like wasm where one should be able to snapshot program state?
ahelwer · · focus · HN ↗