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