Re:The Case for Formal Verification (2013)
by solomatov on Monday April 21, 2014 @02:30AM
(#7620051)
The difference here is that type system in case of agda and coq is the core of the language, it's very similar to what operational semantics does with usual programming languages. The type systems is a logic via Curry-Howard correspondence, with which program correctness is proved. In case of Haskell it's just a software engineering tool which helps you find errors in your program in a semi-automatic way.
[ Parent
| on HN ]
I would say its a sliding scale, I don't think there is a sharp qualitative difference between Idris and Haskell. Haskell programs can also be thought of as proofs, namely proofs that the variables/functions you define have the types you claim they have.
You mention Agda and Coq. Maybe one difference in our viewpoint is that Idris really is designed for general purpose programming. E.g. you can write a program with almost identical structure to a Haskell program.
Re:The Case for Formal Verification (2013)
by solomatov on Monday April 21, 2014 @12:30PM
(#7621899)
>I don't think there is a sharp qualitative difference between Idris and Haskell.
Yes, there's no such a difference. However, in order to use Idris to its full potential, you need to use dependent types. It's just like writing procedural programs in object-oriented or functional language. It's possible, however, it's not a very bright idea.