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

111–120 of 121 posts

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

#111

Post by touisteur »

malisper wrote: post #77
throwaw12 wrote: post #48

Earlier quoted context omitted.

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

GOTO is back ! So glad to see CBMC used. I used to write translators to GOTO for simple code checking and was wondering where the recent state of the art was. Thanks for the pointers.

Did you have a look at why3 and generating verification conditions from Rust or C code (as frama-c does) ?

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

#112

Post by touisteur »

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…

Yes it gets hard really fast. We had a fun (if tongue-in-cheek) exploration of this (proving a sort implementation) with Yannick Moy of SPARK fame some time ago https://www.adacore.com/blog/i-cant-believe-that-i-can-prove...

I only regret not writing the obvious-but-buggy code that "forgot" or added some values and still passed proof...

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

#113

Post by StilesCrisis »

akshayshah wrote: post #56
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.

I'm not sure how to think about what you mean by "almost never." If most commercial software is web frontend + monolithic app code + relational DB, then you may very well be right. That doesn't quite match my professional experience, though - there are so many companies building databases, message queues, filesystems, and similar infrastructure. Sometimes they're internal projects, and sometimes they're commercial pr…

Almost all software is internal "make the business run" software that we never see, or web pages. Very very few engineers would even consider making a new message queue. The crowd here is different than most :)

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

#114

Post by Jtsummers »

teiferer wrote: post #108
Jtsummers wrote: post #104

Earlier quoted context omitted.

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.

> If practice is enough

If that is what you got from my comment, then you did not read my comment.

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

#115

Post by win311fwg »

IshKebab wrote: post #110
win311fwg wrote: post #97

Earlier quoted context omitted.

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!

You may also know of it as standard verification or empirical verification. Regardless of the name, I am sure you can understand the concept as it is exactly of the same intent as formal verification (e.g. you might seek to ensure that a value is an integer between 1 and 10), but absent the formal methods. Of course, just as you can seek to verify that a value is between 1 and 10 you can also simply verify that a value is an integer.

Therefore the possibility of the same dividing line exists in that space as well, but I was wondering if you recognize the same dividing line there, or if it is unique to where formal methods are used?

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

#116

Post by ip26 »

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…

It's a complementary tool that replaces certain difficult types of testing. Viewed this way, you can focus writing formal specification for things which are easy & clear to formally specify. "this returns sorted lists" is, for example, a simple property. Other examples might be the O(n) performance of your algorithm. Meanwhile, "every input can be found in the output" might feel too painful to write, so you might compromise on "the output has the same number of elements as the input". This leaves plenty of space for classical testing, while unburdening classical testing from worrying about select classes of bugs.

One other valuable part of formal methods is forcing the author to make claims about their program, and then poking holes in those claims. This process helps the author understand their own code better, and after a process of iteration developing the formal properties that are actually true, you now have a strictly-true external interface specification for the program. This is obviously most-valuable for only certain classes of code, such as libraries or services.

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

#117

Post by ip26 »

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 have also found that equivalent rewrites are one of the best applications for formal. Other examples can be things like vectorizing code while proving the vectorized version is formally identical, refactoring types or objects, or select classes of performance optimization that are not expected to change the output.

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

#119

Post by nickpsecurity »

lioeters wrote: post #85
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…

> designing stuff with TLA+, then feeding the spec into Claude That seems to defeat the purpose of using TLA+ in the first place. It's taking a rigorously logical and proven specification, putting it through a black box (that you don't own and cannot inspect) with indeterminate and unknown process, to get executable code that may or may not have anything to do with the specs. Unless you feed the code back into someth…

Because you can use it to find temporal errors in your software. People in fact do. So, that proves it's worth even if one can't be sure of perfect conformance to the spec.

Far as connecting specs to code, these papers did try to combine Event-B with SPARK Ada:

https://scispace.com/pdf/towards-generating-spark-from-event...

https://rd.springer.com/chapter/10.1007/978-3-031-23119-3_13

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

#120

Post by nickpsecurity »

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.

I believe I proposed that somewhere because it was a small, useful app which often opened malicious payloads. People may or may not fully prove it.

What I thought would be useful is, like Ironsides DNS, a SPARK Ada or other implementation that shows no code injections could ever happen from loading, modifying, or rendering text. That's a useful subset of full verification.

If not that verified, writing things in a memory-safe, concurrecy-safe language covers lots of ground. Rust and Pony put good effort in those areas. In Rust, I think you still had to manually turn on checks for some overflows which hurt performance a lot. So, static analyzers or automated provers for range properties have a performance benefit.

Muen is the largest, production project I know in such a language:

https://muen.sk/

Ironsides was an earlier project:

https://ironsides.martincarlisle.com/

Post reply on HN