[Hardliner66]

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.

[Hermitian909]

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.

[anonzzzies]

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

[lenkite]

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.

[mrkeen]

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!

[abathologist]

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 ;)