Hacker News Reader

Comment by Davidbrcz | Hacker News Reader

Haha.

Formal verification has been around for 40/50 years and we can't say it is a wide success from a industrial point of view. It has some achievements in terms of results/methods and projects checked, but on a daily basis, pretty much no one uses it. We are ages away of having every programmer understanding formal verification and having all programs verified/proved.

Type theory is in a similar situation. Many issues in code could be solved with basic typing algorithms but people and companies favor languages with poor/no typing (python, Javascript).

View on HN

The biggest barrier to adoption of formal verification that I have seen as someone just starting in the field (working through Software Foundations and have a number of projects planned with SPARK, Frama-C, and LiquidHaskell) is the lack of groundwork. Verifying just your own code is complex enough as it is but working with libraries without any clear specification of their interfaces and behaviours makes this so much harder.

I think there is real value in having verified libraries or at least libraries with well defined specs so that interfacing with other code wasn't so tedious. I think this issue is starting to be overcome with regard to the usage of strong type systems. Truly strongly typed languages are finally getting the libraries and communities built up so that they don't seem quite as daunting.

To me, personally, the biggest barrier was lack of a proper introduction with a lot of examples.

I try to break this barrier a bit with my upcoming book: Gentle Introduction to Dependent Types with Idris.

I am very interested in this area but it is impossible for newcomers to get a grasp of it without too much digging. Logical Foundations was OK but I was still missing the theoretical explanation ("why does this tactic work? it is magic!").

So with accumulated knowledge from IRC, forums I hope to address this.

Ooh I'll check this book out once I get through the pile of stuff I have right now.

And as you noted there definitely is a lot of "magic" when it comes to the inner workings of theorem proving tactics. I'm slowly figuring all of that out but like you said it definitely takes time and digging at the moment.

The Little Typer is out soon too https://mitpress.mit.edu/books/little-typer

> Formal verification has been around for 40/50 years and we can't say it is a wide success from a industrial point of view. It has some achievements in terms of results/methods and projects checked, but on a daily basis, pretty much no one uses it.

Formal verification is an essential part of mission critical applications. Therefore, even though they might be few in number - their impact is pretty significant and "wide".

That’s interesting you say that. I’ve known two engineers who worked at JPL and they said that no teams did anything close to formal verification. It’s an incredibly difficult bar to meet

She/He is right and I was a bit cynical in my answer. There are some real industrial projects that used formal methods. I have in mind Airbus with ASTREEE, the Meteor subway system (Paris' subway line 14), Windows' drivers with the SLAM analyzer...

Also, JPL released its model-checker Java PathFinder and hosts every year the Nasa Formal Method conference so I'm pretty confident that at least someone at NASA is interested in formal methods =)

We're definitely moving in the direction. Someone already mentioned Rust, and Typescript is gaining traction in web dev. Banks like Barclays and Standard Chartered already have Haskell teams, and I've noticed more and more Haskell jobs popping up over the years (in London). Scala is already realtively popular.

Formal verification is used in some niche areas (BAE, Galois). Proof Engineer is a real role some companies are looking to fill.

Rust looks like a step towards practical formal verification just because of its design philosophy. I think what we're doing is making engineering languages more and more verifiable as research languages become more and more expressive. Eventually they'll meet in the middle and we'll have formal verification in "real life."

No progress in language theory can fix the fundamental problem of software verification: you need a formal specification to have anything to verify. Who wants to write not only a detailed spec for their code, but a spec that has well defined semantics in some kind of logic? Nobody, that's who. There are very few properties that you care about that are both sufficiently easy to encode in a formal specification and not provided automatically by a safe language.

Even more, software development now involves an assumption of the average manager or customer that some extra feature can be added halfway through.

Is the customer going to be happy with "we've billed $X for a formal spec and that means that we can't make the change that you want, that seems simple without $Y dollars for changes to it and the code." Notice that software methodologies have gone the opposite direction here, with Extreme Programming basically aiming to make all of the programmer's activities revolve around exactly what and only what the customer has actually requested.

But the features are not arbitrary. The vast majority of features are common among many applications, and a template formal spec can be built to satisfy those features. Once formal spec of the building blocks is created, there will only be the small portion of unique code that needs a unique formal spec.

In the logical extreme that can't be the case, because a fully debugged program plus a machine to run it on actually satisfy the definition of a formal specification. Deciding what you want your program to do is the eternal burden of programming, but maybe there's a way to make formal specification at least as easy as regular programming.

But then you already have a perfect implementation that you somehow made without the use of formal verification. But you want to introduce formal verification because translating real-world requirements into a formal language is hard enough that you can't be sure of correctness...

One example of something you'd always like to verify is, "this code does not have undefined behavior". This could be the key to obtaining C speed without C's lack of safety. In fact, in some possibly-formalizable sense, it's probably the ONLY way to do that.

Yes, but: https://news.ycombinator.com/item?id=16442743

You're absolutely right, and that's exactly why I am enthusiastic about these fields. I think there is a ton of potential, and that these fields will be booming once the industry discovers this.

Of course, the point is not to prove every program correct. But it should be feasible to prove security-critical parts correct, especially for large companies.

The biggest problem is that formal verification is about as un-sexy as it gets, since it has no applications an sich.

Not so long ago the same could be said about AI.

And perpetual energy! Guess we, as humans, just aren't great at predicting the future, regardless of what the last 50 years looked like.

> but on a daily basis, pretty much no one uses it.

Maybe not for software but certainly in the hardware world formal verification is common place with mature tools available from multiple vendors.

Machine learning has been around with no success from an industrial point of view until very recently. Until fairly recently, nobody cared and few understood big O notation.

Recent prog languages have added syntax to avoid issues such as "off by on error" (generator etc...), TDD is slowly becoming a standard everywhere. The next step to improve quality in software is formal verification IMO. There is quite a bit of research in that domain and even some academic program languages integrating it within their syntax.

Reply on news.ycombinator.com