4 ms·

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

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.

anonzzzies 3y ago
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 3y ago
I wish something like Lamport's TLA+ (https://lamport.azurewebsites.net/tla/tla.html https://lamport.azurewebsites.net/tla/tla.html) was supported in modern language compilers - perhaps with annotations/macros and a mini formal DSL.
- mrkeen 3y ago
  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 3y ago
    It's still in pretty early development, but you may be interested in https://github.com/informalsystems/quint 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 ;)
Hermitian909 3y ago
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 3y ago

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 3y ago

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

mrkeen 3y ago
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 3y ago
  It's still in pretty early development, but you may be interested in https://github.com/informalsystems/quint 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 ;)

Hermitian909 3y ago

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.