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

21–30 of 121 posts

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

#21

Post by bluGill »

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 of things I'm doing with that list that are not sorting.

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

#22

Post by tombert »

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 along and wait for me to stop talking. I've had several managers say "they'll look into it", which was such an obvious lie that I don't know why they even bothered.

I've "snuck in" TLA+ usage a few times. I gave up on getting anyone else to use TLA+, but as I've gotten more senior-level, I have been given a fair bit more leeway on how I approach projects and as such I have been able to budget myself a day or two to model some of the less-obvious bits of concurrency.

All that said, I have had some luck with designing stuff with TLA+, then feeding the spec into Claude and getting that to implement the actual executable code. Maybe I'll be able to convince an employer that's a good use of time now.

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

#23

Post by honr »

yoshuaw wrote: post #17
ndriscoll wrote: post #8

We do. It's called a type checker. Every "formally verified" system is going to be partially verified. e.g. you might prove your sort procedure sorts, but did you prove its complexity? Under a cost model for integer compares or a cost model for page fetches? Or both? Multi-layer cache page fetch costs? How well you verify just depends on how well you decide to model the problem. Different type checkers have different…

One of my favorite quotes on this topic is: "Type systems are just the parts of formal verification we've figured out how to make fast."

Thankfully this is no longer strictly true. So, I think the quote needs a slight adjustment, "Type systems and $THING are just ...", but $THING is not very well defined yet. Between "linters", and other relatively fast AST-based rule enforcers, some of which looking at higher order behavior, I think we now have an amalgamation of formally verified concepts that we can consider fast enough and sufficient exercised in practice that we are ever closer to widespread formally and dependably verified software.

Still, it's a long journey, and academic formal verification would always be, by design, a few steps ahead of what the industry can do efficiently in practice.

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

#24

Post by eru »

StilesCrisis wrote: post #18

Because there is almost never a business need? Most programs don't need to be rigorously perfect. If they did, LLMs wouldn't be as popular as they are right now. If you're dealing with medical equipment or space flight, maybe there's a need. But usually the goal is to make errors _inexpensive_ to find and fix, not theoretically impossible.

The ironic thing is that LLMs are what will make formal methods feasible.

First: LLMs find so many bugs and security holes in software right now. So you pretty much have to prove your stuff correct, if you don't want to get hacked into.

Second: LLMs make it much easier to apply formal methods. Just ask Claude to prove your stuff in Lean or whatever, no PhD required anymore.

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

#25

Post by plastic-enjoyer »

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.

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

#26

Post by malisper »

excitedrustle wrote: post #16
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 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 for the empty string. This means on some platforms Postgres SELECT '(,5)'::tid; will error and others will accept it.

2) Postgres missed an overflow check in it's cash type[2]. When running SELECT '-92233720368547758.08'::money / (-1)::int8; some platforms will error and other's will return the MIN value. Postgres does check for this for some of the other cash related functions, but it missed it for one of them.

3) When hashing the "char" type Postgres will cast a char to an integer[3]. On some platforms char is signed and on others it's unsigned. This means the hash of a char can be different depending on the platform. If you are using a hash index or hash partitioning on a char and move your DB from x86 to arm, the hashes will differ and your index/partitioned tables become corrupted. Note that this is special char type that you have to refer to by "char" that is separate from the typically used CHAR(n) type which is what you typically use, hence this would never come up under real usage.

The common pattern with all of these is they rely on C behavior that differs across platform (integer overflow, char signedness, strtoul). Rust is better about having more consistent behavior across platforms so these cases get flagged when the Rust code and the C code differ.

[0] https://github.com/postgres/postgres/blob/REL_18_3/src/backe...

[1] https://github.com/postgres/postgres/blob/REL_18_3/src/backe...

[2] https://github.com/postgres/postgres/blob/REL_18_3/src/backe...

[3] https://github.com/postgres/postgres/blob/REL_18_3/src/backe...

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

#27

Post by forinti »

SCdF wrote: post #3

In most industries that need software made for them it's hard enough to get people to care about spending enough time on informal methods let alone formal ones. I simply don't think most of the industry has had the breathing room and respect for engineering for this pattern to develop.

I think programmers in general do not give much thought to the level of engineering required for a task.

Mostly, there's too little, but there are many cases when there's too much. I see people writing tons of tests for corporate software that will be used by a couple of people and will have to be updated regularly anyway.

Building a hut is not the same as building a skyscraper, but we don't really have guidelines for different software projects. No methodology I've ever seen distinguishes types of projects by complexity.

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

#29

Post by tombert »

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 can be difficult to know if your algorithm is correct, especially without the confounding variables that you get with a "real" programming language. Is my program broken because of some memory allocation quirk? Is it broken because of some peculiarity with how pthreads are dispatched? Or is my design wrong? Being able to work at an abstract level at least can check the last part.

Of course, though, you are correct that formal methods aren't silver bullets.

Post reply on HN