Comment by antonvs
3 years ago
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.