Hacker News Reader

Comment by scythmic_waves | Hacker News Reader

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.

View on HN

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.

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.

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

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.

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.

Why3 ‘extends’ OCaml with similar features as well

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.

Reply on news.ycombinator.com