News for hackers. Stuff that matters.

A comment on The Case for Formal Verification (2013). Parent comment

Re:The Case for Formal Verification (2013) by EzraVinh on Monday April 21, 2014 @11:22AM (#7621479)
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.

[ Parent | on HN ]
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.

[ Parent | on HN ]