Hacker News Reader

Comment by intrasight | Hacker News Reader

> Hype: "Formal Verification is a great way to write software. We should prove all of our code correct."

> Shower: Extensive literature review showing that formal methods are hard to learn, extremely expensive to apply, and often miss critical bugs.

Glad you had the caveat "Written in 2000". What was hard and perhaps not worthwhile in 2000 has changed. Computers are a bit faster and software is more pervasive.

A colleague of mine was involved in the formal verification of a really tricky cellular network bug. That was around year 2000. It was hard but was still necessary and successful.

GM has a buggy car. That wouldn't have been an issue in 2000. Now it's an issue that forced them to withdraw a car from the market after about two weeks. Not saying that formal methods could have for sure avoided that, but I suspect that it very well may have.

View on HN

I think the author should have expanded a bit upon "extremely expensive to apply", because that phrase is technically true but really hides the actual problems with formal verification and why it is seldom used in practice.

People unfamiliar with formal verification think it means "the code is provably correct", but that's not what it does. Formal verification can prove that your code correctly implements a specified standard. You still have to define and write that standard. And that's where the problems begin:

- Standards themselves can have bugs, or the standard you wrote is not what you actually wanted. Note that this is the same problem that often occurs in code itself! You've just pushed it up a level, and into an even more arcane and less-debuggable language to boot (formal standards are generally much, much harder to write, debug, and reason about than code)

- The standard is constantly changing as feature requests come in, or the world around you changes. Modern software engineering mostly consists of changing what you or somebody else already built to accommodate new features or a new state of the world. This plays very badly with formal verification.

Formal verification can work in areas where you have a long time to do development, or where your problem space is amenable to having a formal standard (like math problems). In most other cases it just runs completely opposite to the actual problems that software engineering is trying to solve.

A lot of the types of formal methods that Hillel Wayne (the author) writes about are the opposite of what you describe—you write a specification which is provably correct, and then it's up to you to translate that specification into code. The error-prone part is the translation more than the specification.

It amounts to the same thing: it takes a long time to develop, the specification can get out of sync with the code, and once out of sync you now have no provable characteristics of the new system.

Though this does make me wonder: If there exist some formal methods that can prove that code implements a standard, and others that can prove that the standard is correct, it seems like there ought to be something in the middle that can prove both.

I'm not sure I agree with your conclusion. There's a large grey area in the formal methods space where general software engineering thrives (in my opinion). Especially the "lightweight formal method" variety. I doesn't go for complete proofs, but instead pursues a style of exhaustive (or something that approximates it) checking. Going down this route puts a very positive design pressure on your applications as well as your thinking in general.

The big pay off in formal methods is learning to think abstractly (imho). Even if you don't make a full blown model, sketching out the problem in something like TLA+ can be extremely valuable just by forcing you to think about the modeling independently of code. Even in the world of general software engineering, being able to reframe requirements as temporal invariants has felt something like a super power.

According to my colleague, who is deep into that space, formal methods are also very useful in finding bugs in specifications.

> Formal verification can work in areas where you have a long time to do > development, or where your problem space is amenable to having a formal > standard (like math problems). In most other cases it just runs completely > opposite to the actual problems that software engineering is trying to solve.

Have you actually tried, or is this just the standard line?

I've heard this from people I've worked with, and when I followed up to ask what kinds of projects they've worked on with Agda, Idris, Coq, Lean, whatever, they had nothing.

I don't have anything either, other than that I've toyed around with some of these systems a little bit. But it seems to me like there's a lot of potential in dependently-typed programming, and we just don't have a lot of experience with it -- which is fine, but that's a very different situation than what seems to be the standard line, "all formal methods take a ton of time and are only viable in a few niche projects" (what are people imagining here? NASA space probes and stacks of binders? really it doesn't seem obvious to me, I'm not trolling).

The issues with the Blazer have nothing to do with formal methods; no other automaker has had the problems GM has had.

Those problems have been with every EV it has put on the market since the Bolt (which was developed in South Korea, and largely not by GM.)

https://insideevs.com/news/702126/ultium-platform-owners-gm/

It's just sheer incompetence and mismanagement in one company.

Reply on news.ycombinator.com