3 ms·

Idris isn't very far from Haskell. Perhaps that's already pretty far for practical purposes for a lot of people. Idris does actually try to be a programming l

by sshine 4y ago

Idris isn't very far from Haskell. Perhaps that's already pretty far for practical purposes for a lot of people. Idris does actually try to be a programming language and not just a proof system. F* tries to be like Standard ML with proofs. It really is ergonomic for an ML. But if you haven't written Standard ML (or OCaml), this feels very much like you're a mathematician trying to prove facts about programs rather than run programs.

valenterry 4y ago
> Idris isn't very far from Haskell. From my experience it's very far apart. I know that there is Haskell Liquid but that is still does not make it a real value-dependent type-system, even though in many cases it allows a similar expressiveness. If we talk in the context of programming paradigms, I don't think I would count Haskell in.