Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Why don't people use formal methods? (2019)

hillelwayne.com

Post reply on HN
Print view View original

101–110 of 121 posts

Re: Why don't people use formal methods? (2019)

#101

Post by antonvs »

1970-01-01 wrote: post #57

When I interviewed at AWS, I asked this question directly to their formal methods expert. Her response was two-fold: 1. All our code changes too much, we wouldn't be able to formalize it before it needed to change. 2. We already did this where we could, you just don't see it. I didn't get the job and remain very skeptical on both answers. I think they just didn't have enough power internally to change the move fast a…

Why are you skeptical on point 1?

For anything more complex than standard static type checking[], they're almost certainly correct.

[] or, say, Haskell-level type checking. Which admittedly, AWS is not doing.

Re: Why don't people use formal methods? (2019)

#102

Post by pocksuppet »

Jtsummers wrote: post #96
pocksuppet wrote: post #94

Earlier quoted context omitted.

Actually, sorting a list is an example of something really easy to specify: for each pair of two elements, the one that comes first is less than or equal to the one that comes second.

> for each pair of two elements, the one that comes first is less than or equal to the one that comes second. That's the property that the result is sorted, but not that you've performed the desired task of sorting a particular list. You also need a post-condition saying that each item in the original is in the destination and with the same number of occurrences . If you just require that the result be sorted, then t…

Aaaaaand now it's a good demonstration of why specifications are not as easy as they seem.

Re: Why don't people use formal methods? (2019)

#104

Post by Jtsummers »

pocksuppet wrote: post #102
Jtsummers wrote: post #96

Earlier quoted context omitted.

> for each pair of two elements, the one that comes first is less than or equal to the one that comes second. That's the property that the result is sorted, but not that you've performed the desired task of sorting a particular list. You also need a post-condition saying that each item in the original is in the destination and with the same number of occurrences . If you just require that the result be sorted, then t…

Aaaaaand now it's a good demonstration of why specifications are not as easy as they seem.

It mostly just takes practice. A good way to get into it is with property-based testing. It's less formal, but you end up expressing many of the same things (you're at least expressing the post-conditions, if not the rest of the things needed for a proof). With practice, you'll start to understand your systems better, and things like what I wrote up will come to you more easily when analyzing and designing them.

To move towards formal proofs of code, I like Leino's Program Proofs (uses Dafny), one of the more approachable tutorials on the subject.

Re: Why don't people use formal methods? (2019)

#105

Post by shermantanktop »

fultonn wrote: post #65
shermantanktop wrote: post #40

Earlier quoted context omitted.

Execs will often hand-wave away complexity as being irrelevant detail. And sometimes it is - especially if an urgent directional decision is needed. The key skill - which is rare - is knowing exactly how much analysis to do. Formal methods are appealing because they suggest that full analysis is possible. But formally proved programs can still have bugs!

I think you probably got this, but spelling it out anyways for future readers. The conceptual gap I'm referring to here has nothing to do with formal methods per se . It's just an analogous problem with the quanta of information required to state the spec vs the quanta of information required to state the implementation. Namely: once your problem has enough of a certain type of essential complexity, there's not a hug…

Right, it's a map with a scale of 1:1.

A map with a scale of 100:1 is perfectly useful for navigation. It's just no good for specifying the terrain you want to build with any precision.

Re: Why don't people use formal methods? (2019)

#106

Post by rstuart4133 »

s_dev wrote: post #2

https://blog.janestreet.com/formal-methods-at-jane-street-in... I thought this article from Jane Street makes a nice complimentary pairing.

And this pairs nicely with Jane Street's observation that agentic coding changes the formal proof equation: https://news.ycombinator.com/item?id=49064854

Formal proofs of code are almost beyond the capabilities of the best human programmers (3.7 lines per day!), but LLMs can bash out code at an amazing pace. It's often crap, sadly, but the proof they are bashing out is the hard bit. If possible at all, the task is EXPTIME. Verifying the proof is only P, so when it's wrong you tell the LLM to do it again. A stable agentic loop is what makes it possible. The results in the article I linked to speak for themselves.

Re: Why don't people use formal methods? (2019)

#107

Post by pdimitar »

mike_hock wrote: post #46
malisper wrote: post #13

I recently came across a use case where formal methods were incredibly helpful. I've been rewriting Postgres in Rust and am currently focusing on correctness. The biggest challenge is that there's so much surface area to cover. Postgres has over 3000 user-facing functions, ranging from regular expression matching to JSON iteration to computing the gamma function. About half of these functions are simple pure function…

> I've been able to formally verify that the Rust behavior is identical to the Postgres C behavior I thought you wanted to get rid of the bugs!

The tongue-in-cheek tone aside, every good rework begins with mostly replicating the old program and only then fixing bugs.

But I've seen brave reworks too. They get my standing ovation when pulled off right.

Re: Why don't people use formal methods? (2019)

#108

Post by teiferer »

Jtsummers wrote: post #104
pocksuppet wrote: post #102

Earlier quoted context omitted.

Aaaaaand now it's a good demonstration of why specifications are not as easy as they seem.

It mostly just takes practice. A good way to get into it is with property-based testing. It's less formal, but you end up expressing many of the same things (you're at least expressing the post-conditions, if not the rest of the things needed for a proof). With practice, you'll start to understand your systems better, and things like what I wrote up will come to you more easily when analyzing and designing them. To m…

> It mostly just takes practice

If practice is enough to get a formal system to be correct then why are we doing all this in the first place? Just write correct software! Oh, you can make mistakes? Exaclty! Just like when writing the spec.

Re: Why don't people use formal methods? (2019)

#109

Post by deterministic »

People do use formal methods. Type checking is a simple form of formal methods.

Some languages have type systems that are advanced enough to prove code correct (LEAN/Agda/...)

Other examples are seL4 (a proven correct micro kernel used on millions of devices), CompCert (a proven correct C compiler used by Airbus), TLA+ used by AWS etc. There are many more examples.

So yes it is not main stream but it is being used where it counts.

Re: Why don't people use formal methods? (2019)

#110

Post by IshKebab »

win311fwg wrote: post #97
IshKebab wrote: post #95

Earlier quoted context omitted.

As I said, it's a continuum. I'm drawing the line somewhere further along it than Rust's type system.

Understood. In dynamic verification, does that same line hold? Or would you say it is it unique to formal verification? If so, why?

First I've heard of "dynamic verification" tbh. Is that just everything that isn't static analysis? Not sure I understand the question!
Post reply on HN