Hacker News Reader

Comment by ndriscoll | Hacker News Reader

We do. It's called a type checker. Every "formally verified" system is going to be partially verified. e.g. you might prove your sort procedure sorts, but did you prove its complexity? Under a cost model for integer compares or a cost model for page fetches? Or both? Multi-layer cache page fetch costs? How well you verify just depends on how well you decide to model the problem. Different type checkers have different modeling features.

This is a more useful perspective; it's not "we do/don't use formal methods," but instead "how can I more precisely model my domain?" Helpfully, if you model your domain well, code tends to be obvious/write itself.

View on HN

One of my favorite quotes on this topic is:

"Type systems are just the parts of formal verification we've figured out how to make fast."

Thankfully this is no longer strictly true. So, I think the quote needs a slight adjustment, "Type systems and $THING are just ...", but $THING is not very well defined yet. Between "linters", and other relatively fast AST-based rule enforcers, some of which looking at higher order behavior, I think we now have an amalgamation of formally verified concepts that we can consider fast enough and sufficient exercised in practice that we are ever closer to widespread formally and dependably verified software.

Still, it's a long journey, and academic formal verification would always be, by design, a few steps ahead of what the industry can do efficiently in practice.

The field really needs more popularizers. I mean people or projects who can do "advertising" like, "if you add our linter to your CI/CD pipeline, you'll never have X class of bug ever again!"

given your experience on the topic, i'm curious: do you think that the reason we haven't figured out how to make other parts of formal verification fast is that, in general, programming languages expose each individual machine operation in the code, so the verification surface area is the combinatorial set over that? i've been working on a low level high opinion language, and its verifications are able to be checked in an extremely tight loop, largely because of the structure of the language itself.

Or, at least how to make easy to create. (What is related to fast in complex ways.)

I think there's an element of this which really breaks down to the type system being the part of formal verification that we've figured out how to do during the course of implementation.

Software engineers (myself included, over the years) often argue their real value isn't just writing code, its figuring out the gaps in requirements and how to resolve them. Sometimes that engineering process gets turned back into a formal spec. But much more often, the implementation functionally becomes the spec and contains many details that were never present in the original statement of the requirements.

Formal verification techniques in general are a harder sell until we get the industry to a point where there's broader agreement that what we call "implementation" is often a blurry mix of spec development, prototyping, and actual implementation all happening at the same time.

Reply on news.ycombinator.com