Or Idris dependent types, which allows you to prove properties of any value, not just numbers.

Afaik refinement types (e.g. LiquidHaskell) are bit more appropriate than dependent types for this sort of thing

Plus, Nim supports formal proof natively

https://nim-lang.org/docs/drnim.html

Hey, great for Nim. Though I hope they're not /too/ tied to z3. Why3 seems to be the standard SOTA tool for proof: it can harness lots of different SMT solvers (each with their strengths and weaknesses) including z3, cvc4, alt-ergo, but also specific solvers (grappa?). It is at the heart of Frama-C and Spark2014.

I also think that not having executable contracts by default (and defining whether you want them in your final program or not - see ghost code) is going to be a pain point in the future. I don't know nim enough to see if the syntax for provable properties is different from nim's ordinary syntax but I feel that it can also be a trap, to have your users learn yet another language for proof.

I'm hoping for the best here, and I must say, I'm quite happy to see other languages/environment jump in !

Some years ago you had only industrial support for Frama-C, Spark, and some academic success around JML? I don't know Eiffel's Eve enough to say whether I would consider it 'mature'. Nowadays with the work on Rust by Alastair Reid we're getting some new energy in the domain. Great!

> I hope they're not /too/ tied to z3

If you mean having a hard dependency on z3 at compile time or something similar - no, it's not. :)

I was more thinking of having written the whole verifier to fit/please z3. It can be hard/daunting to move to more 'generic' SMT drivers if done late in a project.