Which language to use for general programming with dependent types?

coq
idris
agda

#22

http://www.ats-lang.org/

It’s an SML clone, where from what I understand you have to prove that the code is safe, both memory wise, and like in general.

So you get rust level performance, multicore, dependant types, and SML syntax.


#23

If you do not want to write manual proofs, dependent type systems are probably not for you yet. (Although you may find out that you actually can write proof, even maybe like to do it, once you realize thanks to these systems how that is very similar to programming.) If you want to write high-assurance programs, I would highly recommend trying Why3/WhyML as a first step: WhyML as a language is very close to OCaml (essentially a subset), and it supports program verification with (mostly-)automated proofs. (Dafny is closest in usage to Why3, but the programming language is farther away from OCaml.)


#24

The closest to what I was looking for is Idris.
I want to prototype research software using dependent types,
to see how productive it is.
I will give a try at Idris on a small/toy project in the coming months.