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

61–70 of 121 posts

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

#61

Post by baq »

empath75 wrote: post #59
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've been using TLA with claude code at work and it roughly takes twice as long, but it's already _fast_ to get claude to produce code and this prevents a lot of rework.

Been having LLMs make TLA+ models since the winter and it does work wonders for complex stuff, I guess for the same reason it works for humans: the process of building the model helps when designing the code even if the model is thrown away later (I keep mine though)

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

#62

Post by sethhochberg »

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…

I think there's an element of this which really breaks down to the type system being the part of formal verification that we've figured out how to do during the course of implementation.

Software engineers (myself included, over the years) often argue their real value isn't just writing code, its figuring out the gaps in requirements and how to resolve them. Sometimes that engineering process gets turned back into a formal spec. But much more often, the implementation functionally becomes the spec and contains many details that were never present in the original statement of the requirements.

Formal verification techniques in general are a harder sell until we get the industry to a point where there's broader agreement that what we call "implementation" is often a blurry mix of spec development, prototyping, and actual implementation all happening at the same time.

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

#63

Post by marcosdumay »

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

Or, at least how to make easy to create. (What is related to fast in complex ways.)

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

#64

Post by IshKebab »

win311fwg wrote: post #36
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 l…

It's a continuum... but I would say even Rust's type system is not in the realms of "formal verification". I think you need at least some kind of refinement types so you can say "an integer between 1 and 10" before you can stake even a vague claim to "formal verification".

So I don't think you can say it's common in the software world.

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

#65

Post by fultonn »

shermantanktop wrote: post #40
fultonn wrote: post #32

Earlier quoted context omitted.

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!

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 huge delta between "a sufficiently specific description of the problem" and "the source code that solves the problem". The complexity of a sufficiently specific prompt approaches the complexity of the actual solution. At that point, the former does not have the purported benefit and the latter has a lot of huge benefits (determinism, modularity, etc).

When one is operating in that regime of problems, proposing that one can substantially automate the software engineering function has a real "I am not able rightly to apprehend the kind of confusion of ideas that could provoke such a question" feel to it.

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

#67

Post by phafu »

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…

While there is certainly quite a bit of truth to what you say, I have a few counter arguments:

> same order of magnitude as the code implementing it

I believe mathematically formulating what an algorithm should do is very often orders of magnitue simpler than implementing it. As we know from the halting problem, it is easy to specify what the algorithm should do, but it is provably impossible to implement such an algorithm, so there the ratio of complexity is infinite ;)

Also, the huge advantage of a specification is that it is much more compositional than actual code. As the article states, one can just specify (and verify) that the code never crashes totally independent from what the code otherwise should be doing. So one can easily look at each part of the specification and understand why it is a desirable property piece by piece, in much larger isolation than the monolithic totality of the code.

Even more, with a formal specification one can (and probably should, when it gets too compilcated) verify by proof that the spec is internally consistent, i.e. that no part contradicts the requirements of another.

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

#68

Post by epolanski »

forinti wrote: post #27
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 fo…

I know few 100% unit test coverage, strictest typing to encode invariants fellas who's app is consistently broken and product makes less money than the bakery in my village.

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

#69

Post by epolanski »

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…

Software engineers are rarely engineers at all, and pretty much never know anything about computer science.

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

#70

Post by win311fwg »

IshKebab wrote: post #64
win311fwg wrote: post #36

Earlier quoted context omitted.

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

It's a continuum... but I would say even Rust's type system is not in the realms of "formal verification". I think you need at least some kind of refinement types so you can say "an integer between 1 and 10" before you can stake even a vague claim to "formal verification". So I don't think you can say it's common in the software world.

Specifying that a value must be an integer between 1 and 10 is most certainly further along the continuum than only specifying that a value must be an integer, but both define a theorem about the program that can be validated. How is the latter not formal verification? It's the same thing, only differing by degree.
Post reply on HN