4 ms·

I've not had as much time to look into formal verification as I'd like and this blew me away lemma LemmaFromToBytes(v: nat) ensures FromBytes(ToBytes(v

I've not had as much time to look into formal verification as I'd like and this blew me away lemma LemmaFromToBytes(v: nat) ensures FromBytes(ToBytes(v)) == v { // Dafny does all the work! } The compiler can _prove_ one function is the inverse of another? That's so cool. Also I disagree with some of the other posts dismissing the usefulness of this kind of thing. I grant that formally verifying every little piece of my code would be overkill. However, I absolutely want certain core pieces of my application formally verified. I'm gonna have to play with Dafny at some point.

adjav 3y ago
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.
- toastal 3y ago
  Why3 ‘extends’ OCaml with similar features as well
- lenocinor 3y ago
  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.
- xigoi 3y ago
  I'm trying to learn Lean and like it, but it's terribly lacking documentation.
  - lenocinor 3y ago
    The lacking good docs was what stymied my group too.
Hardliner66 3y ago
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.
sn9 3y ago
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/ https://mitpress.mit.edu/9780262546232/program-proofs/
novok 3y ago
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.

adjav 3y ago

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.

toastal 3y ago
Why3 ‘extends’ OCaml with similar features as well
lenocinor 3y ago
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.
xigoi 3y ago
I'm trying to learn Lean and like it, but it's terribly lacking documentation.
- lenocinor 3y ago
  The lacking good docs was what stymied my group too.

Hardliner66 3y ago

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.

sn9 3y ago

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/ https://mitpress.mit.edu/9780262546232/program-proofs/

novok 3y ago

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.