4 ms·
> ACL2 is old and crusty We have many new shiny FM tools now, though, that are far closer to regular programming languages. In particular, Agda, Coq, Isabelle
by dons 14y ago
> ACL2 is old and crusty
We have many new shiny FM tools now, though, that are far closer to regular programming languages. In particular, Agda, Coq, Isabelle are fairly easy to pick up for people with an FP background (rather than a formal methods background).
The breakthroughs in SMT solver performance have been astounding to watch, and their use for "brute force" FM is certainly growing.
Of course, verified code is still many times the cost of unverified code, but the gap is coming down.
- jetti 14y agoI'm using Coq for a formal method class and the CoqIde is a piece of software that falls into this category. If I have two files open and I run a search, there is a good chance that the CoqIde will crash and I'll lose my work. I've worked around it by saving my work before I search but I shouldn't have to worry about searching in an IDE