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

71–80 of 121 posts

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

#71

Post by teiferer »

bluGill wrote: post #21
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 have a deeper problem. When I'm calling sort() it is useful that it returns a sorted list. However my program rarely has sorted lists of any sort in any requirement. My requirements are around the features my users care about. Sure the list of employees that I need to display needs to be sorted (sometimes by hire date, sometimes by title, sometimes by name - and often combinations of the above), but there are a lot…

In which way is that a "deeper" problem? What you are doing with that data can also be expressed as a formal spec.

Sorting is just used as an example everywhere because everybody knows exactly what we are talking about without having to explain a lot, it has a somewhat easy solution space and everybody has implemented some form at some point, likely in school, for the same reasons . Of course real world software is more complex that that but that's not the point.

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

#73

Post by teiferer »

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 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

Thanks for this fantastic extension of my example, because that is still incomplete Input [2, 1, 3] and output [1, 1, 1]. Matches your revised spec, still wrong.

If multiple smart software engineers get this simple problem wrong, then how many corpses are burried in the average formal spec? Unless it has gone through rigorous review and testing. Which could have been done to the code to be verified, by the way.

You need that the output is a permutation of the input.

I agree with your larger point though.

Maybe as a last comment, few people actually write tricky concurrent stuff. Like lock-free data structures. There are niches where you gain a lot with a thorough formal spec and verification. But in many cases people should just use sth off the shelf that is already safe, or just use a big lock instead of trying to be smart.

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

#74

Post by mrkeen »

taybin wrote: post #41

I would love to see an example of a proof for something like a text editor. How can people be expected to do this when the examples are always trivial toys, like array sorting? Show me a formal proof of something that in the trenches programmers can copy from. A proof of a basic todo list or something like that.

> A proof of a basic todo list or something like that.

Just using a verb here would be a first step toward rigorous thinking. A proof that a todo list does what?

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

#75

Post by mrkeen »

dahart wrote: post #20
antonvs wrote: post #9

Earlier quoted context omitted.

> similar to how we can answer "python" to that question when the question is about general programming An ironic claim in the context of formal methods.

Out of curiosity, why’s that? I don’t know formal methods nor the relationship to python.

The most widely available, useful, and best-bang-for-buck formal method is using a good type system.

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

#76

Post by mjw1007 »

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…

I think the postgresql maintainers don't claim to support moving a database from x86 to arm without a dump-and-reload. The docs tend to say "same hardware architecture". Though if they don't intend to support this case I think it's a shame if the pg_control checks allow the server to start after such a migration.

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

#77

Post by malisper »

throwaw12 wrote: post #48
malisper wrote: post #26

Earlier quoted context omitted.

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…

these are impressive findings, I am curious what was your process to convert existing code to formal verification languages like TLA+. My basic understanding was to verify high level abstractions (e.g. transport ACK, fsyncs and so on), but verifying this deep probably requires complete verification of stdlib methods used by Postgres, otherwise how can you pinpoint culprit is the sscanf?

Right now I'm only doing very small simple functions. Kani[0] takes care of translating the code to an intermediate representation for me. It converts the Rust code and C code into a GOTO program[1] which verifiers can then run on top of

[0] https://github.com/model-checking/kani

[1] https://model-checking.github.io/cbmc-training/cbmc/overview...

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

#78

Post by teiferer »

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…

Well put, thank you.

One thing I should say though is that the spec has the luxury of being free of some constraints that the implementation has. For example, the functional spec of a sorting function could describe the shape of the required output without having to say how to arrive there. Or in more complicated cases it could afford an exponential simple algorithm to say that the actual implementation must be functionally equivalent. That may make it simpler because it's free of having to run in linear or whatever time complexity.

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

#79

Post by malisper »

mjw1007 wrote: post #76
malisper wrote: post #26

Earlier quoted context omitted.

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…

I think the postgresql maintainers don't claim to support moving a database from x86 to arm without a dump-and-reload. The docs tend to say "same hardware architecture". Though if they don't intend to support this case I think it's a shame if the pg_control checks allow the server to start after such a migration.

> I think the postgresql maintainers don't claim to support moving a database from x86 to arm without a dump-and-reload

I would be very surprised by that because that means replicating a database between the two platforms would lead to corruption.

btw, this bug breaks dump-and-reload too. If you use partitioning, each partition is dumped and restored individually. In this case though, you'll get an error when you try to restore the data because it's trying to put data in the wrong partition. That's better corruption, but still an issue.

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

#80

Post by Merkur »

Interesting read, thank you. I share your goal, and I think with AI- coding proving code right has become more relevant than ever.

What prevents that we, just move the goal post? Moving the bug from code to spec? The spec must always be simpler and more easily to understand and debug than the code. But in praxis that means it can’t be fully specific in most of the use cases?

Post reply on HN