Comment by nanolith
3 years ago
> That's probably possible now.
It's definitely possible now. Formal methods continues to shift from the theoretical, academic, and difficult to the practical. There are model checkers based on SMT solvers that can be used today to enforce function contracts. It is getting easier to extract software for more complicated logic (e.g. data structures and algorithms) using proof assistants.
I can't really speak for ML and other forms of AI, because I have not attempted to design such a system with formal methods in mind. But, traditional software can be made safer with formal methods today.
I'm a big fan of formal methods, but we have to recognize that their use is still very limited, and that's a function of the difficulty of using formal methods effectively.
The idea that they could be used to prove the kind of properties claimed in the paper, essentially by throwing AI at the problem, is hand-waving of the fluffiest order.
That's not what I claimed. The parent poster was talking about non-AI applications.
Regarding their use today, model checking is indeed quite usable -- today -- for verifying function contracts. It is more difficult to use model checking for recursion, loops, data structures, algorithms, or cryptography. But, calculus of constructions can be used to build up proofs of these things and extract viable software.
This field has significantly progressed over the past 20 years and the past decade.
My point is that despite what you're saying about the possibilties of formal methods, it doesn't have any bearing on the claims in the OP paper.
More bluntly, it's irrelevant to the discussion.
With LLMs revolutionising programming, maybe there's not much room left for using formal methods. Postmortem:
The problem that needed solving: Computer programs make mistakes because they're too literal and they don't understand a programmer's intentions.
The problem they tried to solve instead: Computer programs make mistakes because we don't write out mathematical formulas detailing how programs should behave, and mathematically prove that our programs obey said formulas.
Problems they ignored: First, the problem they tried to solve wasn't the problem they were given -- this would be OK if the researchers produced usable methods on time. Second, if the formula is sufficiently detailed, it becomes effectively an executable program in its own right, and so you're back to square one. Thirdly, the formula might not capture a programmer's intent either.
How they tried solving it: Spent 60 years not producing nearly any working product, except for final-year-projects done by their Bachelor's students. Published endless papers in conferences and journals*. Spent a few decades telling the software industry that it should drop everything and use formal methods.
Assessment: Like a lot of software engineering fads that are promised as panaceas, this probably had a niche application somewhere, but its problems were ignored by its advocates and it underdelivered.
* - Some of the theory they worked on was interesting in its own right: Type theory, constructive logic, computerised proof assistants, computable topology (and domain theory), substructural logics, some category theory, etc. I just think that now that LLMs are revolutionising programming, it's too late for this stuff to deliver anything to Software Engineering, and this stuff turned out to be of purely intellectual interest.
> The problem that needed solving: Computer programs make mistakes because they're too literal and they don't understand a programmer's intentions.
> The problem they tried to solve instead: Computer programs make mistakes because we don't write out mathematical formulas detailing how programs should behave, and mathematically prove that our programs obey said formulas.
The problem is documenting the intent of a rule-based system and confirming that it acts as expected.
As every programmer knows, thoroughly defining intended behavior is the meat of impmenting said behavior.
Often refining the intent based on thinking through or implementing intermediate solutions.
This is not just because of the difficulty to make computers behave the way we want to, it includes the difficulty of defining how we want it to behave, too.
There is no silver bullet that can remove ambiguity from human instructions, or always guess "correctly" when missing clear instructions.
Because by definition, what is correct?
LLMs and other generative AI methods are nowhere near replacing the need for better reasoning about software, especially in safety critical systems.
Maybe, but I'm not totally convinced: If an AI understands intentions, then it can carry out our intentions without us doing any traditional programming, specified using only plain English, especially in a safety-critical situation where this would probably be the best thing to do. Anyway, how would formal methods measurably help here [EDIT: By here, I mean security critical applications]? And have they shipped anything yet in that area, given that we've been waiting 60 years for them to do that?
The answer is partially yes, admittedly, with TLA+. What else have they shipped?
6 replies →