5 ms·

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

by tempire 12y ago

nardi 12y ago
What do you mean by "not widely available"? Just as examples, Coq and Idris are both free: https://coq.inria.fr https://coq.inria.fr http://www.idris-lang.org/ http://www.idris-lang.org/ Did you mean they're not in wide use?
- coldtea 12y ago
  Just too languages being available != "tools". Where are the toolchains, IDEs, libs, etc for those?
- lmm 12y ago
  I'm trying to install and use Idris as we speak. It seems to require learning two other languages (Haskell, PowerShell) first.
  - mcguire 12y 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.
    - lmm 12y ago
      > All of the dependently typed languages, like Coq, that I've seen have not been very good programming languages, in my opinion. Yeah, that's why I'm looking at Idris - it seems like the only one that's oriented towards practical programming. I did eventually get it installed, but it's tough going doing anything with it when you don't know Haskell tbh.
      - codygman 12y ago
        > Idris - it seems like the only one that's oriented towards practical programming Whether you like ATS or not, it's very oriented towards practical programming. Also, ATS mostly looks bad IMO because of the style the author uses. I still haven't fully formed an opinion on ATS though. Idris does seem really cool and stuff like enforcing time/space usage through the type system excites me.
        mcguire 12y ago
        I'm not sure whether my issue with ATS is the style of the author or its type system, although I suspect the former. ATS is based on ML (the author started with Dependent ML), but the code has a very imperative feel, leading to statements like "let () = expr() in ..." and "let x = ... in ()". The stuff at http://www.ats-lang.org/Examples.html http://www.ats-lang.org/Examples.html is just hideous, by the way.
        codygman 12y ago
        I agree with you, though I think it is because of the authors style. Check out some of Chris Done's ats code examples in a more appealing style: https://gist.github.com/chrisdone/c23251e8b975dc805876 https://gist.github.com/chrisdone/c23251e8b975dc805876
        codygman 12y ago
        Here's just a small translation of the ats examples[0] page. ----------------- Copying File ---------------- Authors version: fun fcopy ( inp: FILEref , out: FILEref ) : void = let val c = fileref_getc (inp) in if c >= 0 then let val () = fileref_putc (out, c) in fcopy (inp, out) end // end of [if] end (* end of [fcopy] *) ----------------- Naieve Fibonacci ---------------- My version: fun fcopy ( inp: FILEref, out: FILEref ) : void = let val c = fileref_getc (inp) in if c >= 0 then let val () = fileref_putc (out, c) in fcopy (inp, out) end end Authors version: fun fib ( n: int ) : int = if n >= 2 then fib (n-2) + fib (n-1) else n My Version (not sure if valid!): fun fib ( n: int ) : int = if n >= 2 then fib (n-2) + fib (n-1) else n ----------------- Fast Fibonacci ---------------- Authors Version: fun fibc ( n: int ) : int = let fun loop (n: int, f0: int, f1: int) = if n > 0 then loop (n-1, f1, f0+f1) else f0 // end of [loop] in loop (n, 0, 1) end // end of [fibc] My Version: fun fibc ( n: int ) : int = let fun loop (n: int, f0: int, f1: int) = if n > 0 then loop (n-1, f1, f0+f1) else f0 in loop (n, 0, 1) end 0: http://www.ats-lang.org/Examples.html http://www.ats-lang.org/Examples.html
AKluge 12y 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 12y 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.

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

by tempire 12y 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.

nardi 12y ago

What do you mean by "not widely available"? Just as examples, Coq and Idris are both free: https://coq.inria.fr https://coq.inria.fr http://www.idris-lang.org/ http://www.idris-lang.org/ Did you mean they're not in wide use?

coldtea 12y ago
Just too languages being available != "tools". Where are the toolchains, IDEs, libs, etc for those?
lmm 12y ago
I'm trying to install and use Idris as we speak. It seems to require learning two other languages (Haskell, PowerShell) first.
- mcguire 12y 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.
  - lmm 12y ago
    > All of the dependently typed languages, like Coq, that I've seen have not been very good programming languages, in my opinion. Yeah, that's why I'm looking at Idris - it seems like the only one that's oriented towards practical programming. I did eventually get it installed, but it's tough going doing anything with it when you don't know Haskell tbh.
    - codygman 12y ago
      > Idris - it seems like the only one that's oriented towards practical programming Whether you like ATS or not, it's very oriented towards practical programming. Also, ATS mostly looks bad IMO because of the style the author uses. I still haven't fully formed an opinion on ATS though. Idris does seem really cool and stuff like enforcing time/space usage through the type system excites me.
      - mcguire 12y ago
        I'm not sure whether my issue with ATS is the style of the author or its type system, although I suspect the former. ATS is based on ML (the author started with Dependent ML), but the code has a very imperative feel, leading to statements like "let () = expr() in ..." and "let x = ... in ()". The stuff at http://www.ats-lang.org/Examples.html http://www.ats-lang.org/Examples.html is just hideous, by the way.
        codygman 12y ago
        I agree with you, though I think it is because of the authors style. Check out some of Chris Done's ats code examples in a more appealing style: https://gist.github.com/chrisdone/c23251e8b975dc805876 https://gist.github.com/chrisdone/c23251e8b975dc805876
        codygman 12y ago
        Here's just a small translation of the ats examples[0] page. ----------------- Copying File ---------------- Authors version: fun fcopy ( inp: FILEref , out: FILEref ) : void = let val c = fileref_getc (inp) in if c >= 0 then let val () = fileref_putc (out, c) in fcopy (inp, out) end // end of [if] end (* end of [fcopy] *) ----------------- Naieve Fibonacci ---------------- My version: fun fcopy ( inp: FILEref, out: FILEref ) : void = let val c = fileref_getc (inp) in if c >= 0 then let val () = fileref_putc (out, c) in fcopy (inp, out) end end Authors version: fun fib ( n: int ) : int = if n >= 2 then fib (n-2) + fib (n-1) else n My Version (not sure if valid!): fun fib ( n: int ) : int = if n >= 2 then fib (n-2) + fib (n-1) else n ----------------- Fast Fibonacci ---------------- Authors Version: fun fibc ( n: int ) : int = let fun loop (n: int, f0: int, f1: int) = if n > 0 then loop (n-1, f1, f0+f1) else f0 // end of [loop] in loop (n, 0, 1) end // end of [fibc] My Version: fun fibc ( n: int ) : int = let fun loop (n: int, f0: int, f1: int) = if n > 0 then loop (n-1, f1, f0+f1) else f0 in loop (n, 0, 1) end 0: http://www.ats-lang.org/Examples.html http://www.ats-lang.org/Examples.html

AKluge 12y 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 12y 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.