Comment by nardi
12 years ago
What do you mean by "not widely available"? Just as examples, Coq and Idris are both free:
Did you mean they're not in wide use?
12 years ago
What do you mean by "not widely available"? Just as examples, Coq and Idris are both free:
Did you mean they're not in wide use?
I'm trying to install and use Idris as we speak. It seems to require learning two other languages (Haskell, PowerShell) first.
PowerShell? That's a new one....
I haven't used Idris, but as a proof assistant, Coq is one of the best computer games I know[1]. As a programming language, it's a very good proof assistant.[2]
[1] Really! It's fun. I've found the resulting proofs impossible to read, though. The closest description I can make is that they're programs for a stack machine; reading those is not a skill I've developed.
[2] All of the dependently typed languages, like Coq, that I've seen have not been very good programming languages, in my opinion. Except for ATS, which I don't think is a good programming language for different reasons. But I really like it, anyway.
> All of the dependently typed languages, like Coq, that I've seen have not been very good programming languages, in my opinion.
Yeah, that's why I'm looking at Idris - it seems like the only one that's oriented towards practical programming. I did eventually get it installed, but it's tough going doing anything with it when you don't know Haskell tbh.
4 replies →
Just too languages being available != "tools".
Where are the toolchains, IDEs, libs, etc for those?