← Back to context

Comment by tempire

12 years ago

It's not too slow, it just takes discipline that most developers/companies don't have, primarily because the tools aren't widely available.

11 comments

tempire

Reply
AKluge  12 years ago

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.

  • mafribe  12 years ago

    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.

nardi  12 years ago

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?

  • lmm  12 years ago

    I'm trying to install and use Idris as we speak. It seems to require learning two other languages (Haskell, PowerShell) first.

    • mcguire  12 years ago

      PowerShell? That's a new one....

      I haven't used Idris, but as a proof assistant, Coq is one of the best computer games I know[1]. As a programming language, it's a very good proof assistant.[2]

      [1] Really! It's fun. I've found the resulting proofs impossible to read, though. The closest description I can make is that they're programs for a stack machine; reading those is not a skill I've developed.

      [2] All of the dependently typed languages, like Coq, that I've seen have not been very good programming languages, in my opinion. Except for ATS, which I don't think is a good programming language for different reasons. But I really like it, anyway.

      5 replies →

  • coldtea  12 years ago

    Just too languages being available != "tools".

    Where are the toolchains, IDEs, libs, etc for those?