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

31–40 of 121 posts

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

#31

Post by win311fwg »

teiferer wrote: post #19

To me, "this returns sorted lists" illustrates the crux. You may know exactly what you want, and you may have a reasonably fast and cheap way to verify your code against a formal specification. But the formal specification needs to come from somewhere and for any non-trivial program its complexity is going to be in the same order of magnitude as the code implementing it. So we are back to writing "code" (which is wha…

> The promise of formal verification

The promise of formal verification (and testing) is essentially the same promise as double-entry accounting. It assumes that if you do the same thing twice that it is unlikely you will screw it up in the exact same way twice. When there is disagreement it tells you that something went wrong, but you still need to look at both sides to determine which one is wrong. There is no such thing as a panacea, of course.

> It's another tool next to testing, not instead of it.

Theoretically it is instead of. They both are trying to solve the exact same problem. The real world with real constraints isn't so neat and tidy, so they don't end up perfectly overlapping.

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

#32

Post by fultonn »

teiferer wrote: post #19

To me, "this returns sorted lists" illustrates the crux. You may know exactly what you want, and you may have a reasonably fast and cheap way to verify your code against a formal specification. But the formal specification needs to come from somewhere and for any non-trivial program its complexity is going to be in the same order of magnitude as the code implementing it. So we are back to writing "code" (which is wha…

I think every formal methods phd student who's interested in adoption of their techniques/tools has a short bout of doubt/depression upon realizing just how large of a surface area for bugs lives in a sufficiently useful specification.

This is deeply related to the conceptual error a lot of executives are currently making around automation in/of their software engineering orgs.

It has always been true that learning some formal methods probably makes you a better programmer in certain ways, even if you never use them. I think it's increasingly also true that learning some formal methods probably makes you a better manager of people/processes that product software.

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

#33

Post by dcminter »

Pretty much every job I've had has involved integrating with highly imperfect, changeable, and inaccurately implemented (and barely documented) third party APIs. That's where most of the work went and I don't see formal methods improving the situation any time soon.

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

#34

Post by mattkrause »

tombert wrote: post #29
teiferer wrote: post #19

To me, "this returns sorted lists" illustrates the crux. You may know exactly what you want, and you may have a reasonably fast and cheap way to verify your code against a formal specification. But the formal specification needs to come from somewhere and for any non-trivial program its complexity is going to be in the same order of magnitude as the code implementing it. So we are back to writing "code" (which is wha…

I mean, just for this particular example, you could certainly also add a check that the sorted list is the same length as the input list. That said, your broader point is more or less correct. I think the advantage of something like TLA+ is that the specs can generally be more abstract and as such the checks can be more exhaustive than you would likely get with regular "code". With concurrent code, in particular, it…

I think you'd want to specify that every element in the original list is present in the sorted list (and in the same number, in case of ties).

And of course, that raises the issue of what do you want to do about ties....

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

#35

Post by tombert »

plastic-enjoyer wrote: post #25
tombert wrote: post #22

I've been a big nerd for formal methods for quite awhile, and have been broadly unsuccessful in getting employers onboard. I have pretty cynical opinions as to the "why" of this, largely involving the fact that the vast majority of software engineers refuse to learn anything that they weren't explicitly taught in college , but regardless of the reason whenever I have tried proposing TLA+ in the past, people will nod…

> I have pretty cynical opinions as to the "why" of this, largely involving the fact that the vast majority of software engineers refuse to learn anything that they weren't explicitly taught in college, but regardless of the reason I think it's not only SWEs, but general persons that goe to college primarily to get a job, without having a natural curiosity for things.

Probably true, I've just only ever worked in the software engineering world so I cannot speak about anything else.

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

#36

Post by win311fwg »

IshKebab wrote: post #10

I think everyone knows the answer already - it's too hard to be worth it for most problems. The article doesn't disagree with that and was a good read anyway. Don't skip it because you already know the answer. IMO the reason is way more on the "it's too hard" side than "it isn't worth the effort". Formal verification is extremely common in the silicon hardware design world, despite its extreme cost (the tool licenses…

Formal verification is also extremely common in the software design world, to be fair. Most programming languages in use have at least a primitive type system and even those that historically didn't are gaining them (e.g. Typescript, Python gradual typing, etc.)

The question is, as always, to what degree do the returns start to diminish. The Rust crowd laughs at Go's level of formal verification and says that their level of formal verification is the right level, but then the Lean crowd laughs at Rust's level of verification and says that their level of formal verification is the right level. The universe laughs at all of them. For crowds so concerned about mathematical proofs, it is funny that they end up right back at gut feeling.

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

#38

Post by appplication »

malisper wrote: post #26
excitedrustle wrote: post #16

Earlier quoted context omitted.

> I found 4 different Postgres bugs. Bugs in the upstream Postgres C implementations? Did you report them or submit patches? I'm curious to see what you found!

Yep, I did submit bug reports. This was on Tuesday. I don't see a public copy of the mailing list that has my bug reports yet. The four bugs were: 0) When parsing a macaddr[0], Postgres uses sscanf with %x. %x can wraparound. This means SELECT '10000000aa:bb:cc:dd:ee:ff'::macaddr; will return aa:bb:cc:dd:ee:ff. 1) When parsing a tid[1], Postgres uses strtoul. The return value of strtoul is different across platform f…

Very cool project and good finds. What do you see as the end state for your project - do you think pg has a path to upstream, or would this be a fork?

Without knowing anything about the pg team, I would assume they would be hesitant to even consider an under the hood switch, just from a risk management perspective, regardless of test coverage and formal verification. But I could be wrong.

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

#40

Post by shermantanktop »

fultonn wrote: post #32
teiferer wrote: post #19

To me, "this returns sorted lists" illustrates the crux. You may know exactly what you want, and you may have a reasonably fast and cheap way to verify your code against a formal specification. But the formal specification needs to come from somewhere and for any non-trivial program its complexity is going to be in the same order of magnitude as the code implementing it. So we are back to writing "code" (which is wha…

I think every formal methods phd student who's interested in adoption of their techniques/tools has a short bout of doubt/depression upon realizing just how large of a surface area for bugs lives in a sufficiently useful specification. This is deeply related to the conceptual error a lot of executives are currently making around automation in/of their software engineering orgs. It has always been true that learning s…

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!

Post reply on HN