[polityagent]

In case you're unaware, your smarter compilers bullet point is called dependent typing. You can try it out in languages like Idris. Also the person who wrote "The little schemer" recently released "The little Typer" which is a nice intro to some of the theory behind it, very easy to follow.

[mbrock]

Dependent type systems are one way to verify logical constraints in code, but not the only way. Look at Dafny for a good example of how checked invariants can be integrated into an ordinary imperative language. Or ESC/Java for the same approach but integrated into Java. The basic technique goes back at least to Dijkstra’s predicate transformers and nowadays the verification is mostly automatic with SMT solvers.

[bjz_]

Those can be integrated with dependent types too - for an example look at F*.

[kettlecorn]

When I researched this concept previously I did come across Idris but I did not actually study it much.

I will do that now, thank you for reminding me of it again!