> Unfortunately, people have been focused on the "dynamic" typing (i.e., no type checks) side of things for so long that static checking lags behind in usability

The longer I see things like mypy and typescript evolve, I’m actually really glad that people have been focused on gradually typing dynamic languages. As far as I can tell, really useful contracts (or really flexible types) are super burdensome in the most general cases (e.g. `refl` brain twisters in dependent types), but still insanely useful in frequent cases. It reminds me of what people say about static typing’s benefits and burdens.

So I’m hoping to see the gradual typing equivalent for contracts and verification. Start with usefulness and add a spectrum of optional safety that the programmer can ignore or use as they see fit. Personally, at least, that would be my ideal scenario.

Kotlin has some functionality for this that help the compiler. A good example is the isNullOrBlank() extension function on String? (nullable String). It has a contract that treats the string as not null after it returns false. So if you do a null check, it smart casts to a non nullable string without generating a compile error.

There are a few more variations of that in the Kotlin standard library and you can write your own contracts as well. There's just not a whole lot you can do with it other than stuff like this. But it's useful.

Types in Idris sound like the contracts you mention. I learnt about them in the book "Type-Driven Development with Idris".

There is a fairly close relationship between a dependently typed language, like Idris, and 'contracts' (really, pre- and post-conditions plus other propositions) in languages like Ada/SPARK, Dafny, and Frama-C.

The major differences are that most (all?) dependently typed languages are functional and require the programmer to prove the correctness of the contract in (an extension of) the language itself, while the others typically use special annotations in normal Ada/C/a generic ALGOLish language and dump the proof onto external tools like SMT solvers, all resulting in a more 'normal' programming experience.

I think liquid types, ala Liquid Haskell are a preferable middle ground in this scenario. The SMT is built into the type checker and the refinements are limited to a linearly decidable proof fragment. Dominic Orchard has done some work generalizing the capabilities of these types of refinement by showing that the refinement fragment need to just be a semi-ring structure and the SMT can still resolve. This would cover a large portion of contracts and not impart the development process in large part.

There is ATS as an example of an imperative language with dependent types.