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

81–90 of 121 posts

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

#81

Post by fultonn »

teiferer wrote: post #78
fultonn wrote: post #65

Earlier quoted context omitted.

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

Yes, it's probably the most important trick in formal methods. Often surprisingly difficult to make it actually work, but when it does you can end up with a powerful tool.

In a past life I spent a lot of time on that sort of thing for control systems and RL. Spec says what not to do, reward says what to do, implementation can be arbitrarily complex wrt the spec.

There are many opportunities for an analogous move in LLM-assisted software engineering.

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

#82

Post by tombert »

teiferer wrote: post #73
tombert wrote: post #29

Earlier quoted context omitted.

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

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

Yeah, I agree with the sibling comment somewhat that you'd probably want to make sure that all the elements are included as well. I do think you'd get much more exhaustive testing at the algorithm level than you'd get with "regular" code, even with unit tests. But sure, your broader point is right, passing the spec doesn't guarantee that everything is "right", and it can be misleading.

I feel like formal methods help when you're optimizing concurrent software more than anything. About a year ago I had a project that I wrote a naive version that was too slow because the initial version had a ton of lock contention. I wanted to rewrite it to use a less lock-heavy system but I wasn't 100% sure that my idea on how to speed it up would actually work. I ended up doing my design in PlusCal before I wrote the new version, and there were issues with my initial version (where in certain cases we could lose vital records), but fortunately I was able modify the design to fix it. I translated my design to Java and my new version was way faster.

I don't agree that a big lock is a good idea, but I do agree that people should, in general, use off the shelf things to handle this instead of trying to be cool. That said, occasionally I get into situations where those libraries aren't a good fit, or what they're doing is too slow.

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

#83

Post by mjw1007 »

malisper wrote: post #79
mjw1007 wrote: post #76

Earlier quoted context omitted.

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…

The physical replication docs say "the hardware architecture must be the same", though they don't define "architecture".

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

#84

Post by tombert »

epolanski wrote: post #69
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.

Yeah, I've always been that "annoying math guy" for pretty much my entire career.

This has always irritated me, because I'm not entirely sure what engineers feel that they bring to the table over a high school kid who bought one of those "learn C++" books. I always thought the value-add was supposed to be a better understanding of the theory and computer science and internals of how computers work, but that was evidently wrong.

I've noticed that the "software engineers bragging about not knowing any math" trend appears to be dying, so that's cool, but now it has been replaced with the even more depressing "software engineers don't need to even need to know how to code anymore because you can just ask Claude Code to do it".

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

#85

Post by lioeters »

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 something to verify that it corresponds with the specs? Is there nothing that can turn the specs into executable code directly and deterministically? Why involve a language model at all?

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

#86

Post by wduquette »

I was exposed to Z notation in the late 80's, and could not for the life of me see how to apply to my work as a junior programmer. But the distinction the OP makes between Design and Code Specification was lost on me then (and, I think, on the folks I knew who were looking at Z); and the OP indicates that Z is aimed at Design Specification. As a junior programmer, it's no wonder it was lost on me.

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

#87

Post by tombert »

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…

I'm not familiar with any general purpose TLA+->regular code exporter. I think there are a few proof of concepts but as far as I'm aware nothing that has been seriously suggested for production.

I do audit the code it generates, but ultimately all I'm concerned about is the algorithm a lot of the time and since the transformation it's been generally ok. I feel like coding errors and implementation-of-the-spec errors are different things, and of course this would be an issue even if it were humans writing the code.

If you use something like Isabelle then that has direct Scala and Haskell export. I like Isabelle but personally I find that for actual engineering problems it is often too cumbersome and TLA+ is much easier to get something done.

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

#88

Post by Jtsummers »

poly2it wrote: post #30

For me, I wish the systems languages I am interested in could couple with legible verification systems, but alas, the world of formal methods seems disjoint. The only way to get a satisfactory development experience seems to be to learn Lean.

> The only way to get a satisfactory development experience seems to be to learn Lean.

Or SPARK, if you want to stick to systems languages.

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

#89

Post by taybin »

mrkeen wrote: post #74
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?

To-does. Just like how a butler buttles.

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

#90

Post by lioeters »

tombert wrote: post #87
lioeters wrote: post #85

Earlier quoted context omitted.

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

I'm not familiar with any general purpose TLA+->regular code exporter. I think there are a few proof of concepts but as far as I'm aware nothing that has been seriously suggested for production. I do audit the code it generates, but ultimately all I'm concerned about is the algorithm a lot of the time and since the transformation it's been generally ok. I feel like coding errors and implementation-of-the-spec errors…

> would be an issue even if it were humans writing

I see what you mean, that the conversion of TLA+ specs to code is error-prone in any case, regardless of who or what does the conversion.

From what I've heard, an advantage of Lean over other major theorem provers is that it can generate actual executable code (apparently C), so you get the best of both worlds: formally proven specification and the implementation. In that context, I can imagine the use of language models to assist in the generation of specs, tests, and documentation - while a (formally specified) program deterministically compiles the specs to code, or maybe interprets the specs directly to run it as code.

Post reply on HN