Let’s say I want to do system/backend programming using a language
with dependent types (just to give it a try).
Which one of those would be the best considering
agility of the programmer (I want to do software prototyping) and performance of the final executable (I want the final program to execute reasonably fast).
Coq
Agda
Idris
something else?
I don’t care so much if the ecosystem is poor in terms of libraries,
because I can write most things from scratch for my research, if needed.
Of the languages that you cite, Idris seems to be the more practical alternative to do systems programming, because of the built-in FFI. I’m not sure there is any such thing in Agda or in Coq (I guess the equivalent would be to axiomatize the FFI and map it to whatever OCaml function during extraction).
The ATS language advertises itself as having dependent and linear types, and allowing “the programmer to write safe low-level code that runs in OS kernels”. Never tried it though.
What kind of properties of your programs are you interested in proving with dependent types?
To be clear, I am not interested in writing proofs (and I would be quite incompetent at that).
I just want to write code, and have a high confidence about what the code is doing.
Or, the only proof I want is that we go from 'a to 'b.
I would like to give a try at dependent types so that 'a
and 'b can encode a lot of properties about the things
I am manipulating (molecules).
Is the size of the user base of those languages known?
I would guess Coq has a lot of users.
Maybe the size of the user community is a good heuristic for
the production-ready state of a language.
I think these are mostly users who use if for proofs, not for “general” programming. But there are multiple books on “general” programming with Idris, so I think I would check out Idris or ATS first.
Hmm I would not be too optimistic about that, unless the properties carried by your molecules are rather simple and the proof that your function preserves these properties can be discharged automatically by the system that you use. My typical interaction with these systems is that your program will essentially have to encode the proof of the property that it should verify (which is the usual Curry-Howard gospel). Maybe you can elaborate a bit about the properties of your molecules?
I think you can try any of these three languages to get a first feeling as to what programming in these systems involve in terms of effort. Also, maybe you can glance at this book which is based on Coq: http://adam.chlipala.net/cpdt/cpdt.pdf. If you expect full automation, my advice would be to forget about it.
This book is about certified programming.
Which makes me think about writing programs hand in hand with a mathematical proof.
That’s not what I want to do (I know the programmer productivity of such approaches is not for prototyping, it is for certification of software).
I just want to write programs and let the type system prove what can be proved about them.
(Note : I’m not an active user of any of the systems, only spent some free time learning one of them, so salt etc)
Programming with dependent types is same as writing proofs (by Curry-Howard correspondence), as brought up by @igarnier
So the distinction between writing proofs and dependent type programming is not very meaningful in principle, and it usually boils down to usability of the system/language and your use cases.
And full automation is normally not possible due to undecidability of logic systems.
Also, it’s may not always be clear if dependent types have a clear advantage over verifying properties separately.
Since you care more about automation, I’d just use platforms geared toward automated program verification(e.g. WhyML, Frame-C, Ada SPARK, Dafny) rather than limiting myself to dependently typed languages.
Lastly since you’re trying to use it on molecules, I’m assuming you’re trying to do scientific simulations. I have no idea if formal verification has any place in scientific computation where code is usually lean and floating point error seems to be a bigger problem.
“F* (pronounced F star) is a general-purpose functional programming language with effects aimed at program verification.”
“F*'s type system includes dependent types, monadic effects, refinement types, and a weakest precondition calculus.”
EDIT: I missed your “just to give it a try” part in your sentence, whoops. In that case, then both Idris and Agda seem like a sane choices, Coq is more geared towards theorem proving than programming.
That is what programming with dependent types is for. If you don’t want that, then you don’t want to be working in a dependently typed language in the first place.
Not necessarily. In some of these systems, you just write the theorems (type annotations) and the system writes the proves for you (type checking).
Plus, types are theorems in disguise. The casual user may not need to be aware that they are stating theorems. (I expect that few OCaml users think about types that way.)
That’s a dream, not a reality. No system is very proficient at general theorem proving yet. There are excellent and interesting tools of course, but ultimately if you work in Coq or any of the rest you spend a lot of time proving things.
Coq’s type system is too powerful for that, though. Once you get to fully general dependent types (say the Calculus of Constructions and above) you no longer have algorithms to do what you want.
I disagree. I think he’d learn Coq pretty quickly, and think that the spirit of the syntax is quite similar. I learned Coq before I learned OCaml and I found OCaml much more natural as a result of knowing Coq first. I bet the opposite direction holds.
Also, there’s now the really good “Software Foundations” series to self-study Coq.
