3 ms·

For those of you not familiar with Haskell, it's worth pointing out that types and proofs are equivalent (with caveats). What this means in practice for Dafny i

by moomin 10y ago

For those of you not familiar with Haskell, it's worth pointing out that types and proofs are equivalent (with caveats). What this means in practice for Dafny is that anything you can do in it can equally be expressed in a language like Idris (with footnotes). Equally, it means that the trickiness encountered in heavily typed functional programming languages is carried over directly to working with program verifiers. At that point, it's more a case of what's easier to grok and work with. I mention this, because I see a lot of people who dismiss something like Idris out of hand saying they want correctness checking, not realizing they're basically equivalent.

amelius 10y ago
But wouldn't it be much more cumbersome to check correctness using a type-system?
- moomin 10y ago
  In short: no. It's exactly as cumbersome. If you look at the other comments you'll see plenty of people that found it hard to work with. Equally, if you look at Idris mailing lists you'll find people who love it. Another way of looking at it is which is easier to grok: imperative or functional flow.
  - pron 10y ago
    It's complicated. Basically, verifying programs is hard and pretty cumbersome regardless of the formalism, and the differences in the theory don't matter too much for most things people do. Having said that, making practical use of dependent types is currently behind proof tools for direct logic (in terms of automated provers, model checking etc.). What people sometimes do is start with direct logic expressed as a contract (say, like in Dafny, Java with JML or Ada SPARK), run automated tools on those (SMT solvers), and if the solvers fail, generate obligations for a logic based interactive prover or a dependent type one, at which point the differences matter even less. But working completely within a dependently typed language is currently unrecommended unless you just want to learn or play a bit, or unless you're an expert. Dependent types are just not yet "production ready".
- tomp 10y ago
  Yes. The main advantage of program verifiers (e.g. Dafny) is that there's no (or very little) type/term division. A runtime function `+` is the same as the proof/mathematical function `+`, runtime numbers are mathmatical numbers, etc. (it gets a bit more complicated with equality AFAIK). As a result, in Haskell you have to reimplement the whole (Peano) integer arithmetics again in the type system to prove e.g. array bounds checks, whereas Dafny automatically maps between proofs and code. I think that Haskell is slowly doing away with this (they're unifing the term and proof language). I think that Idris completely unifies the two. The only difference that remains then is that Dafny uses an automated theorem prover (Z3), whereas in Haskell/Idris you have to do proofs by yourself.
  - moomin 10y ago
    Idris has pluggable peoof strategies, so whilst it's not doing it all for you, in theory you could plug Z3 into it.
qznc 10y ago
It is types≘theorems and programs≘proofs. https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon...
- moomin 10y ago
  Yes, sorry.
tom_mellior 10y ago
> For those of you not familiar with Haskell, it's worth pointing out that types and proofs are equivalent (with caveats). What this means in practice for Dafny is that anything you can do in it can equally be expressed in a language like Idris (with footnotes). For those of you not familiar with Brainfuck, it's worth pointing out that it's Turing complete and hence equivalent to Haskell (with caveats). What this means in practice for Haskell is that anything you can do in it can equally be expressed in a language like Brainfuck (with footnotes). Footnote: The programming and proving styles of Dafny and Idris are (roughly) as similar as the programming styles of Haskell and Brainfuck. [What I am trying to say is this: Just because two systems do "verification" and are hence "equivalent", it's silly to suggest that they are pragmatically similar.]

by moomin 10y ago

amelius 10y ago

But wouldn't it be much more cumbersome to check correctness using a type-system?

moomin 10y ago
In short: no. It's exactly as cumbersome. If you look at the other comments you'll see plenty of people that found it hard to work with. Equally, if you look at Idris mailing lists you'll find people who love it. Another way of looking at it is which is easier to grok: imperative or functional flow.
- pron 10y ago
  It's complicated. Basically, verifying programs is hard and pretty cumbersome regardless of the formalism, and the differences in the theory don't matter too much for most things people do. Having said that, making practical use of dependent types is currently behind proof tools for direct logic (in terms of automated provers, model checking etc.). What people sometimes do is start with direct logic expressed as a contract (say, like in Dafny, Java with JML or Ada SPARK), run automated tools on those (SMT solvers), and if the solvers fail, generate obligations for a logic based interactive prover or a dependent type one, at which point the differences matter even less. But working completely within a dependently typed language is currently unrecommended unless you just want to learn or play a bit, or unless you're an expert. Dependent types are just not yet "production ready".
tomp 10y ago
Yes. The main advantage of program verifiers (e.g. Dafny) is that there's no (or very little) type/term division. A runtime function `+` is the same as the proof/mathematical function `+`, runtime numbers are mathmatical numbers, etc. (it gets a bit more complicated with equality AFAIK). As a result, in Haskell you have to reimplement the whole (Peano) integer arithmetics again in the type system to prove e.g. array bounds checks, whereas Dafny automatically maps between proofs and code. I think that Haskell is slowly doing away with this (they're unifing the term and proof language). I think that Idris completely unifies the two. The only difference that remains then is that Dafny uses an automated theorem prover (Z3), whereas in Haskell/Idris you have to do proofs by yourself.
- moomin 10y ago
  Idris has pluggable peoof strategies, so whilst it's not doing it all for you, in theory you could plug Z3 into it.

qznc 10y ago

It is types≘theorems and programs≘proofs. https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon...

moomin 10y ago
Yes, sorry.

tom_mellior 10y ago

> For those of you not familiar with Haskell, it's worth pointing out that types and proofs are equivalent (with caveats). What this means in practice for Dafny is that anything you can do in it can equally be expressed in a language like Idris (with footnotes). For those of you not familiar with Brainfuck, it's worth pointing out that it's Turing complete and hence equivalent to Haskell (with caveats). What this means in practice for Haskell is that anything you can do in it can equally be expressed in a language like Brainfuck (with footnotes). Footnote: The programming and proving styles of Dafny and Idris are (roughly) as similar as the programming styles of Haskell and Brainfuck. [What I am trying to say is this: Just because two systems do "verification" and are hence "equivalent", it's silly to suggest that they are pragmatically similar.]