(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.
One language not mentioned:
- “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.