> 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

> 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.]