You might want to look in Lean 4 at some point too. A lot of work has gone into making it's theorem solving ergonomic and approachable for average programmers.

Why3 ‘extends’ OCaml with similar features as well

My personal anecdote is that I tried learning Lean 4 last year with a group of other smart and curious programmers, and after a couple of weeks of trying, we failed to make significant progress learning it and stopped. We had much better luck working with Coq instead.

I'm trying to learn Lean and like it, but it's terribly lacking documentation.

The lacking good docs was what stymied my group too.

People always think that using some sort of formal verification is overkill, but then they end up hunting bugs for months that would be trivially detectable in such tools.

Formal Verification tools allow you to write a specification in a common language, that can be checked by a tool. Every time the spec changes, you can instantly verify that all invariants still hold.

Yes, lot of formal verifications are (almost) free and most others are not. But if you at least take the free ones, why not…

I wish something like Lamport's TLA+ (https://lamport.azurewebsites.net/tla/tla.html) was supported in modern language compilers - perhaps with annotations/macros and a mini formal DSL.

And types too :)

I know many words have been spilled over why it shouldn't have them, but I remain unconvinced.

I modelled a trivial traffic light system to make sure the cars and pedestrians didn't have "green" at the same time. And they didn't, because they had "green_light" at the same time. Oops!

It's still in pretty early development, but you may be interested in https://github.com/informalsystems/quint

> It combines the robust theoretical basis of the Temporal Logic of Actions (TLA) with state-of-the-art static analysis and development tooling.

And it is typed ;)

It's a tooling problem. Nearly every comment I read about formal verification being overkill are about proposal to incorporate existing formal verification tools into existing workflows. It is not easy to get an organization to adopt TLA+ in a way that's useful for almost any problem.

Add a language feature like the above to TS and you'd see adoption overnight. Pretty much everyone is happy to let their build system add additional correctness guarantees if its fast enough.

There's actually a brand new textbook on using Dafny at the level of an early undergraduate course: https://mitpress.mit.edu/9780262546232/program-proofs/

IMO this is going up the spectrum from runtime checking to static checking, and it becomes more and more useful when you are writing libraries for mass consumption or working in large codebases with a lot of developers. I wish I had stuff like this at my last job, so much boilerplate to basically guarantee similar stuff statically would be replaced by a few one liner 'ensure' clauses.

I think we will see this feature added to production languages in 3-20 years, hopefully sooner. I think Eiffel had this feature too with their program by contract feature?

It's basically baking in more and more parts of unit tests into the language itself, and a one liner 'ensures' clause is way more concise and stronger of a test than a unit test you have to run separately or an assert that does checks at runtime.

The key issue with static verification is making sure it doesn't get in the way of build speeds, execution speeds and binary size.