Comment by mafribe
12 years ago
It's still too slow today for all but the most security critical applications.
Fortunately there is a lot of work in progress to improve the situation.
12 years ago
It's still too slow today for all but the most security critical applications.
Fortunately there is a lot of work in progress to improve the situation.
It's not too slow, it just takes discipline that most developers/companies don't have, primarily because the tools aren't widely available.
Having learned and put into practice formal proofs of correctness at CMU, I can say that it has fundamentally improved the discipline with which I write production code. The undercurrent of "Is this provably correct" is still there 30 years later, and it produces better code than the more obvious "Will this work here". The cost in production time is small compared to the later revision, refactor and maintenance issues.
I wonder if we are talking about the same things. Do you use Hoare logic or interactive proof assistants when putting "nto practice formal proofs of correctness", and find that that lowers your software engineering costs? I would be surprised if that was the case.
What do you mean by "not widely available"? Just as examples, Coq and Idris are both free:
https://coq.inria.fr
http://www.idris-lang.org/
Did you mean they're not in wide use?
I'm trying to install and use Idris as we speak. It seems to require learning two other languages (Haskell, PowerShell) first.
6 replies →
Just too languages being available != "tools".
Where are the toolchains, IDEs, libs, etc for those?