13 ms·

Formal methods: Just good engineering practice?

179 points by ot 2y ago

robocat 2y ago
I like the quote: “It would be well if engineering were less generally thought of, and even defined, as the art of constructing. In a certain important sense it is rather the art of not constructing; or, to define it rudely but not inaptly, it is the art of doing that well with one dollar, which any bungler can do with two after a fashion.” Arthur Wellington Where is the boundary between finance and engineering? And Engineering is also about making optimal tradeoffs in other dimensions (he mentions time, performance, scalability, sustainability, and efficiency).
- grumpyprole 2y ago
  Absolutely it is about trade offs, sometimes bugs are just an inconvenience and time-to-market is more important. But bugs can result in lost business and even lost lives, for example UK Post Office Horizon. Horizon was built (bungled) on the cheap, but the overall cost of that saving must be dwarfed by the financial cost of the resultant scandal.
  - intelVISA 2y ago
    Wasn't that system claimed 'infalliable'? That outsourced sweatshop must know some CS secrets we don't
- juancn 2y ago
  I like that quote. For me, engineering is applied science for money. That's the main thing. Someone is paying for everything you do. We get into it because we care about the how more than the why, but we end up having to deal with the who is paying for this. The boundary is fuzzy, engineering is heavily influenced by finance, otherwise it's just a hobby. Formal methods are great or an awful decision depending on wether or not they make economic sense for your product or service at your organization's current stage. Amazon EC2? A large, mature org, with products with extremely high fubar potential? Go wild. Your startup where market-fit is not proven? WTF? Are you high? use that money on something else. It's like unit testing, it in general makes great sense if the cost of maintaining the tests is lower than the opportunity cost of slowing down. If you're prototyping something that you'll likely throw away, it may be a bad idea. Once it proves value, you better build a decent test harness. Startups take technical debt because it's cheap when the market fit is not demonstrated (you pay it back later once you have succeeded somewhat). It's a rational decision. You don't need perfection if you're building the wrong thing, first you figure out if what you're building makes sense, then you decide in what to invest. On the other hand, if you're building a deep space probe, a large scale distributed system for hire, or any other thing were a failure is BAD (with capital letters), the extra cost of ensuring correctness is well worth it.
  - hnthrowaway0328 2y ago
    > The boundary is fuzzy, engineering is heavily influenced by finance, otherwise it's just a hobby. This rings true for me. I'm interested in learning things, e.g. how processes work in Windows NT kernel, or how to write a custom memory allocator, instead of creating a product. I do have some passion for a certain product but it is highly personal and won't be shared. Quoting David Cutler, "What I really wanted to do was work on computers, not apply them to problems". I wish I knew this when I was younger.
  - drewcoo 2y ago
    > engineering is applied science for money I thought that was science, not engineering! Money determines the subjects researched, how they're researched, and the results, right?
    - juancn 2y ago
      In science the money is not tied to the utility of the research (or at least no directly tied in most cases). It's possible to get funding to research something completely bonkers, in engineering it's less likely.
  - __MatrixMan__ 2y ago
    I feel like money is too narrow here, but there does need to be some kind of budget involved. For instance, getting the energy output of a nuclear fusion reactor to exceed the energy input is an engineering problem. An energy budget, in that case.
- photochemsyn 2y ago
  Depends on whether the systems you're working on have catastrophic failure modes, or not. In terms of how the responsible parties behave in both realms, it comes down to whether the costs of catastrophic failure can be externalized or not (e.g. government bailouts for chaos in in subprime mortgages or natural gas futures markets, Price-Anderson indemnity for nuclear reactor meltdowns). Miscalculation (see Boeing) can be disastrous. Now if you can't externalize the costs of catastrophic failure, that will be the fundamental constraint on your engineering / finance strategy. If you really don't want your network to be breached, you'll build it around security features, not try to hack them on after the fact. I like to think SpaceX, as a private company without the kind of political heavyweight backers that ULA enjoyed, thus put a lot more effort into avoiding the kind of problems ULA is currently having, for just that reason. Conclusion: take away the government safety nets, and both engineering and finance will perform better? Now about Silicon Valley Bank...
- erik_seaberg 2y ago
  I've seen this stated "Any idiot can build a bridge that stands, but it takes an engineer to build a bridge that barely stands."
  - hn_throwaway_99 2y ago
    In modern days we generally stand in awe of ancient structures that have stood for millennia. But in some sense, many ancient engineers had to drastically overbuild their bridges and other structures because they didn't have the tools to know what the "barely stands" threshold was, so they had to build for a big margin of error when they lacked the tools of precision.
    - erik_seaberg 2y ago
      Yeah, imagine digging up red clay, throwing it in a charcoal furnace, and then hammering it for a while. You can tell you're getting wrought iron, but would you know from one batch to the next whether it's good?
      - j16sdiz 2y ago
        They did that with specification like "use red clay from this village" with "charcoal from that city" in this furnace. It is not scalable, but the quality is quite stable across batches
        fmajid 2y ago
        And then you have the rebar-free Roman lime-pozzolan concrete used in the Pantheon, still standing after 2000 years.
        lesuorac 2y ago
        Not a civil engineer but it sounds like the Romans knew much better then "baked red clay strong". > https://en.wikipedia.org/wiki/Pantheon,_Rome#Structure https://en.wikipedia.org/wiki/Pantheon,_Rome#Structure > The stresses in the dome were found to be substantially reduced by the use of successively less dense aggregate stones, such as small pots or pieces of pumice, in higher layers of the dome. Mark and Hutchison estimated that, if normal weight concrete had been used throughout, the stresses in the arch would have been some 80% greater. Hidden chambers engineered within the rotunda form a sophisticated structural system.[55] This reduced the weight of the roof, as did the oculus eliminating the apex. That said, I'm guessing the Pantheon is in one piece (unlike the coliseum) because it's been used as a church for the past ~1600 years and presumably (similar to Notre Dame) it gets repair as-needed.
- kmoser 2y ago
  Even with an unlimited budget and unlimited time, the difference between good and bad engineering is that a bad engineer won't know where to apply their talents to ensure things won't go wrong in the future. While every discipline in the world is bound by budget and time constraints (even an armchair philosopher has a limited lifespan), that doesn't change the essence of the discipline itself. I think of engineering not just as designing and building things, but also knowing where the limitations are of the thing you're constructing, whether it's purely on paper, in a computer's memory, or from brick and mortar.
- kazinator 2y ago
  You can kill people with bad finance and go to jail; same as engineering.
zeroCalories 2y ago
I do often employ the simple whiteboard methods described, but I've never found the energy to learn and use stuff like TLA+. What fields do people find them useful in?
- 01HNNWZ0MV43FF 2y ago
  I find my biggest problem is interfacing with apis from complex dependencies I can't control, usually OSes and gui libs. I assume there isn't a ton formal methods can do for that unless I set up a VM I can tightly control?
  - buescher 2y ago
    At that point you're probably blowing up your verification/validation space to where it might be intractable , in both a machine and human sense. People have done research work in formal methods all the way down to the assembly level, of course, but could you even write the correctness properties for the software you're describing? Where you can use these methods - think of the part of your program's behavior you can describe with the article's "whiteboard" methods mentioned in the post above - truth tables, decision tables (! TIL), state machines/statecharts. If you can formulate it that way, not only is it easier to reason about and to test, but if you can also work out what would make it correct, you can run it through an automated checker.
- Jtsummers 2y ago
  My only time using TLA+ "in anger" was on an embedded system. There was a problem in the hardware portion and our boss wanted proof it was the hardware and not our software. He didn't accept any of our evidence that it was a hardware flaw, partially because our tests weren't failing 100% of the time. I used TLA+ and ended up with a handful of traces which we were able to recreate with the hardware and some small programs (remove everything our system actually did, just use the busted data bus) to demonstrate the failure, they always failed instead of failing only 90% of the time (shouldn't have been needed, it was obvious the hardware was broken). The TLA+ model started off being a reasonable fidelity model of the specified hardware bus, and then I started messing with it (in a deliberate fashion, altering state transitions) until I got traces and invariant violations similar to the real-world hardware. I've used Alloy for similar things, but only after the fact not during the investigation and as a way to learn Alloy. I'd use them both again (TLA+ especially) if I could convince people it was worth the time, but it can be difficult to get the time to spend on it at work while also meeting other work obligations. I've used TLA+ for some personal projects involving concurrent and distributed systems (toys, nothing notable just playing). I used TLA+ to demonstrate that my design worked as I intended, and then started writing code based on the model.
ChrisMarshallNY 2y ago
I worked for a [Japanese] corporation, that took “formal methods” into overdrive. They made really, really good hardware, but it was extremely painful for us software schlubs. That said, I don’t know if it’s really possible to do really big stuff, with a team, unless you have some degree of formality. Best practices are usually a good place to start, and I would suggest that the degree of necessary formality, is inversely proportional to the experience of the team. If you have a lot of really experienced engineers, in a mature team that has been together a long time, the formality is still there, but doesn’t need to be written down. I usually work alone, or as the sole technical person, in a diverse team. I’m really experienced, and don’t write much down. But I’m also really, really formal. It just doesn’t look like it.
- jxramos 2y ago
  Does it come out instead in PR reviews?
  - ChrisMarshallNY 2y ago
    If I work alone, there aren’t any PRs. But I do spend a great deal of time reviewing my work; often going back, and tweaking and testing, for days. My testing code tends to dwarf my implementation code.
- spankalee 2y ago
  Formal methods is much more specific than formality and writing things down. There's a degree of proof that you achieve with formal methods that you don't even with design documents, reviews, and the usual tests.
  - ChrisMarshallNY 2y ago
    Agreed, but also, “writing things down,” was a bit of a euphemism for the many, many aspects of a formal approach. The main issue is that we can get so wrapped up in the process, that we fail to get anything done. It’s a question of balance.
- 2y ago
erik_seaberg 2y ago
I learned some TLA+ and started reading about Coq, but I was pretty disappointed to learn of the "verification gap" between the the algorithm to be delivered in a normal programming language and the manually-restated algorithm that passed the checker. We need to make a checker's input language ergonomic enough for daily use and then "synthesize" something that runs efficiently while still being known correct, or make a checker understand everyday programs (which, not being so minimalist, probably have a much larger space of reachable states to check).
- ukuina 2y ago
  This is my biggest gripe with verification. I am hoping that LLMs help with inferring intent from a subroutine, then asking the programmer if the inferred intent is complete and correct, and then automatically writing/updating a verification harness.
  - eschaton 2y ago
    What makes you think autocomplete on steroids with no internal reasoning capability or representation of knowledge would be at all useful for inferring intent? Or have you been fooled into thinking an LLM is something like Eurisko/Cyc?
    - pxeger1 2y ago
      Because ideally good code should make the intent obvious from the names and comments, so inferring a full description should really just be an autocomplete task.
      - eschaton 2y ago
        The topic is using an LLM to learn a codebase one doesn’t understand. Does that sound like a codebase that has names and comments from which a full description could be inferred?
    - bubblyworld 2y ago
kazinator 2y ago
Non-software engineering doesn't excessively use formal methods. Only where required. (Like where a system is tightly optimized.) For instance, in electronic engineering, you don't use the most accurate model of a diode at all times. Sometimes it's just a one-way valve. Sometimes, it's just one-way valve with a 0.7V drop (if silicon). In mass production, you will not get the accurate parts needed for the most formal model to be justifiable, and the cost of those parts would not be justified in most of the circuitry.
nanolith 2y ago
In my opinion, most developers should be using bounded model checking if available for their language / platform. This is certainly true for C, Rust, Java, and others. I consider bounded model checking to be "formal methods lite". It provides most of the benefits at a lower cost of entry than using a proof assistant or building constructive proofs. Really, there's little added overhead. Perhaps 30% to 40% more time to build out the function contracts and model checking. Given that this overhead more or less prevents errors that would likely be introduced without it, I think it's a reasonable investment. TLA+ is certainly related, since it uses an SMT solver at its base. I see it as useful for designing algorithms and protocols. A tool like CBMC or Kani provides similar guarantees at the source code level. It's not perfect, as currently CProver does not have direct threading support, but with a reasonable application of method shadowing and function contracts, even things like threading can be anticipated. Using a bounded model checker effectively means changing the design of software to work best with it. This is little different than using concepts like TDD or continuous integration.
- vlovich123 2y ago
  In my experience traditional property checks are pretty difficult to write already (30-40%). I get the sense that a bounded model check would be even more expensive than that, probably into the 2-3x range if not more. I’m talking about meaningfully complex logic, not very simple things.
  - rtpg 2y ago
    It would be interesting to have a workbook of what people consider valuable examples of issues we are trying to solve. Like property checks are sometimes easy to write, when your property aligns well with property checking models! But then time-based stuff like TLA+ ends up working way better, sometimes. There are plenty of canonical examples out there for resolving some issues with types, and having a bunch of one-pagers on issues people hit that people might or might not want to tackle with some flavor of formal method.
  - nanolith 2y ago
    You can write these checks as assertions in your regular source language. It's no more difficult than writing runtime parameter checks, really. There are some complexities, to be fair, but these are mostly around the performance of the model checker. Some things are easy to check, and other things, like loops and recursion, are harder to check. However, this is a matter of optimization, and with practice, this becomes quite easy to deal with.
Almondsetat 2y ago
In my opinion formal methods are what's missing from software engineering to make it a serious engineering discipline. In all other engineering fields you have to produce calculations and "proofs" that your design ought to work. In software engineering everything is basically overcomplicated handwaving.
- atoav 2y ago
  > In software engineering everything is basically overcomplicated handwaving. No, it is worse than that. There are people who claim the proof is the code itself. Just look at it. These are the same kind of people claiming good code needs no documentation. That is like a bridge engineer saying they need no structural calculation because the stability of the bridge is obvious to a certain kind of bridge nerd if they look at it. Only that civil engineers figured out after a few high profile bridge collapses that "trust me bro" isn't good enough and software engineering people are still in the: "trust him, he is a genius"-phase of the field.
  - mrkeen 2y ago
    > There are people who claim the proof is the code itself. Yet this is what emerges when you write a sufficiently detailed proof. The more detail you add to your TLA+ model, the more it looks like just another implementation (albeit untyped, so it's pretty easy to slip errors into).
    - szundi 2y ago
      We should have a TLA+^2 then. Oh the complexity has to be expressed anyway? Uh Oh and users mostly rather suffer from bugs than give up complex desires and features? Uh We’re doomed haha
      - atoav 2y ago
        Isn't that why we have modularization? In the end you can formally verify low level stuff on a per module basis. Knowing that your PNG decoder is formally verified and therefore it is less likely that a user uploads a PNG and gets Runtime Code Execution within that process context isn't worth nothing. And if it allows attackers to get RCE the number of mysterious crashes it might have produced with weird PNGs is probably also non-zero. In the end all security measures are a layered effort and doing a bit formal verification, a bit unit testing, a bit fuzzing etc. is always better than mentally aiming for 100% and not doing anything at all. The question regarding formal verification is: What is the code that is running in the critical domain? Someone who writes safe code will try to minimize the amount of code/executables/complexity in that space. And that domain isn't necessarily a single process, it can be a part in the code, or a process until it dropped privileges etc. If all your code is critical domain it either means you failed to sanitize inputs, everything runs with yolo/root privileges, all of your customers share a single table in your database, your hardcoded admin password is 1234 — or maybe you write code that controls nuclear power plants, airplanes or similar things. But if it is the former, no amount of formal verification will save you anyways because wrote software like a money writes poems: By accident. If the idea of a critical domain is new to those reading this comment, if you never thought about user proviledges when writing an application, please read this as proof of the point that the field of software engineering still lacks in all sort of places and it is in all our interest, both professional and as users/potential victims to improve the situation.
DoingIsLearning 2y ago
Is there formal methods 'tooling' similar to TLA+ that is more targeted to State Machine design and perhaps State Machine Replication?
- nradclif 2y ago
  Model checking can be used to formally verify state machines. See https://en.wikipedia.org/wiki/Model_checking https://en.wikipedia.org/wiki/Model_checking.
- hwayne 2y ago
  https://p-org.github.io/P/ https://p-org.github.io/P/
- rramadass 2y ago
  See Tools section at https://en.wikipedia.org/wiki/Abstract_state_machine https://en.wikipedia.org/wiki/Abstract_state_machine
pjmlp 2y ago
The main issue is that most of these tools like TLA+, live in another dimension, proving something in TLA+, doesn't mean when the algorithm gets actually implemented in C, it still maps to TLA+ as proven. Formal methods need to be like SPARK 2014, or DbC, actually part of the programming language, or being able to generate code in the target language, interop with its libraries ecosystem, and have good quality good with performance, that won't make people want to remove the generated code and rewrite it manually.
- pyrale 2y ago
  For that you would need a proper, well-grounded type system and a language that doesn’t stray from it. Some fp languages are close enough to fit that bill; Rust too is going down this path: its type system was built to make a proof, after all.
- IshKebab 2y ago
  I don't know if that's always the case. My understanding is that TLA+ is really designed to prove properties about algorithms. Knowing that complex algorithms are correct is very useful eventually if it doesn't provide a correct implementation in a real world language. But TLA+ is a bit of an unusual proof language. I think most of them are like you describe: SPARK, Dafny, F*, CBMC, all the Rust ones, etc. I'm not sure about the interactive proof languages (Coq et al), they are too complicated for my normal sized brain.
  - pjmlp 2y ago
    Yes, and making those languages (SPARK, Dafny, F*, CBMC,....) more widespread, the kind of something that everyone expects to be out of the box on their favourite language is how this can eventually gain more adoption, than a few selected companies, or academic research.
- bvrmn 2y ago
  TLA+ helps to find errors in your algorithm. It's a way easier than trying to model the algorithm in terms of end implementation. Too much complexity and state are introduced because of details.
verisimi 2y ago
> What is TLA+? > > TLA+ is a formal language for specifying systems used in industry and academia to verify complex distributed and concurrent systems. Among others, the TLA+ methodology is successfully applied at Amazon Web Services, Microsoft, and Oracle. https://conf.tlapl.us/home/ https://conf.tlapl.us/home/
hresvelgr 2y ago
I think we might potentially be looking at this backwards. There is a great talk by Jack Rusher [1] on why having really slow iteration loops and being too disconnected from running programs creates a desire for theorem proving because it becomes the faster way to arrive at a correct solution. I am of the belief that we need to return to modifying live environments instead of sending code through a lengthy build pipeline. Instead of trying to make live environments secure and durable we got scared and now we have modern CI/CD. [1] https://www.youtube.com/watch?v=8Ab3ArE8W3s https://www.youtube.com/watch?v=8Ab3ArE8W3s
- yencabulator 2y ago
  Good luck trying to get something like Paxos correct by poking at it in a REPL.
  - hresvelgr 2y ago
    Not what I'm advocating and certainly not REPL. When I'm talking about a live environment, I mean something _like_ Pharo [1]. I'm arguing against long compile and deploy loops, not formal verification. [1] https://pharo.org/ https://pharo.org/
treprinum 2y ago
"Beware of bugs in the above code; I have only proved it correct, not tried it. " -- Donald Knuth
ozim 2y ago
Just wanted to post this video link in this discussion: Glenn Vanderburg - Real Software Engineering https://www.youtube.com/watch?v=RhdlBHHimeM https://www.youtube.com/watch?v=RhdlBHHimeM

179 points by ot 2y ago

I like the quote: “It would be well if engineering were less generally thought of, and even defined, as the art of constructing. In a certain important sense it is rather the art of not constructing; or, to define it rudely but not inaptly, it is the art of doing that well with one dollar, which any bungler can do with two after a fashion.” Arthur Wellington Where is the boundary between finance and engineering? And Engineering is also about making optimal tradeoffs in other dimensions (he mentions time, performance, scalability, sustainability, and efficiency).

grumpyprole 2y ago
Absolutely it is about trade offs, sometimes bugs are just an inconvenience and time-to-market is more important. But bugs can result in lost business and even lost lives, for example UK Post Office Horizon. Horizon was built (bungled) on the cheap, but the overall cost of that saving must be dwarfed by the financial cost of the resultant scandal.
- intelVISA 2y ago
  Wasn't that system claimed 'infalliable'? That outsourced sweatshop must know some CS secrets we don't
juancn 2y ago
I like that quote. For me, engineering is applied science for money. That's the main thing. Someone is paying for everything you do. We get into it because we care about the how more than the why, but we end up having to deal with the who is paying for this. The boundary is fuzzy, engineering is heavily influenced by finance, otherwise it's just a hobby. Formal methods are great or an awful decision depending on wether or not they make economic sense for your product or service at your organization's current stage. Amazon EC2? A large, mature org, with products with extremely high fubar potential? Go wild. Your startup where market-fit is not proven? WTF? Are you high? use that money on something else. It's like unit testing, it in general makes great sense if the cost of maintaining the tests is lower than the opportunity cost of slowing down. If you're prototyping something that you'll likely throw away, it may be a bad idea. Once it proves value, you better build a decent test harness. Startups take technical debt because it's cheap when the market fit is not demonstrated (you pay it back later once you have succeeded somewhat). It's a rational decision. You don't need perfection if you're building the wrong thing, first you figure out if what you're building makes sense, then you decide in what to invest. On the other hand, if you're building a deep space probe, a large scale distributed system for hire, or any other thing were a failure is BAD (with capital letters), the extra cost of ensuring correctness is well worth it.
- hnthrowaway0328 2y ago
  > The boundary is fuzzy, engineering is heavily influenced by finance, otherwise it's just a hobby. This rings true for me. I'm interested in learning things, e.g. how processes work in Windows NT kernel, or how to write a custom memory allocator, instead of creating a product. I do have some passion for a certain product but it is highly personal and won't be shared. Quoting David Cutler, "What I really wanted to do was work on computers, not apply them to problems". I wish I knew this when I was younger.
- drewcoo 2y ago
  > engineering is applied science for money I thought that was science, not engineering! Money determines the subjects researched, how they're researched, and the results, right?
  - juancn 2y ago
    In science the money is not tied to the utility of the research (or at least no directly tied in most cases). It's possible to get funding to research something completely bonkers, in engineering it's less likely.
- __MatrixMan__ 2y ago
  I feel like money is too narrow here, but there does need to be some kind of budget involved. For instance, getting the energy output of a nuclear fusion reactor to exceed the energy input is an engineering problem. An energy budget, in that case.
photochemsyn 2y ago
Depends on whether the systems you're working on have catastrophic failure modes, or not. In terms of how the responsible parties behave in both realms, it comes down to whether the costs of catastrophic failure can be externalized or not (e.g. government bailouts for chaos in in subprime mortgages or natural gas futures markets, Price-Anderson indemnity for nuclear reactor meltdowns). Miscalculation (see Boeing) can be disastrous. Now if you can't externalize the costs of catastrophic failure, that will be the fundamental constraint on your engineering / finance strategy. If you really don't want your network to be breached, you'll build it around security features, not try to hack them on after the fact. I like to think SpaceX, as a private company without the kind of political heavyweight backers that ULA enjoyed, thus put a lot more effort into avoiding the kind of problems ULA is currently having, for just that reason. Conclusion: take away the government safety nets, and both engineering and finance will perform better? Now about Silicon Valley Bank...
erik_seaberg 2y ago
I've seen this stated "Any idiot can build a bridge that stands, but it takes an engineer to build a bridge that barely stands."
- hn_throwaway_99 2y ago
  In modern days we generally stand in awe of ancient structures that have stood for millennia. But in some sense, many ancient engineers had to drastically overbuild their bridges and other structures because they didn't have the tools to know what the "barely stands" threshold was, so they had to build for a big margin of error when they lacked the tools of precision.
  - erik_seaberg 2y ago
    Yeah, imagine digging up red clay, throwing it in a charcoal furnace, and then hammering it for a while. You can tell you're getting wrought iron, but would you know from one batch to the next whether it's good?
    - j16sdiz 2y ago
      They did that with specification like "use red clay from this village" with "charcoal from that city" in this furnace. It is not scalable, but the quality is quite stable across batches
      - fmajid 2y ago
        And then you have the rebar-free Roman lime-pozzolan concrete used in the Pantheon, still standing after 2000 years.
        lesuorac 2y ago
        Not a civil engineer but it sounds like the Romans knew much better then "baked red clay strong". > https://en.wikipedia.org/wiki/Pantheon,_Rome#Structure https://en.wikipedia.org/wiki/Pantheon,_Rome#Structure > The stresses in the dome were found to be substantially reduced by the use of successively less dense aggregate stones, such as small pots or pieces of pumice, in higher layers of the dome. Mark and Hutchison estimated that, if normal weight concrete had been used throughout, the stresses in the arch would have been some 80% greater. Hidden chambers engineered within the rotunda form a sophisticated structural system.[55] This reduced the weight of the roof, as did the oculus eliminating the apex. That said, I'm guessing the Pantheon is in one piece (unlike the coliseum) because it's been used as a church for the past ~1600 years and presumably (similar to Notre Dame) it gets repair as-needed.
kmoser 2y ago
Even with an unlimited budget and unlimited time, the difference between good and bad engineering is that a bad engineer won't know where to apply their talents to ensure things won't go wrong in the future. While every discipline in the world is bound by budget and time constraints (even an armchair philosopher has a limited lifespan), that doesn't change the essence of the discipline itself. I think of engineering not just as designing and building things, but also knowing where the limitations are of the thing you're constructing, whether it's purely on paper, in a computer's memory, or from brick and mortar.
kazinator 2y ago
You can kill people with bad finance and go to jail; same as engineering.

zeroCalories 2y ago

I do often employ the simple whiteboard methods described, but I've never found the energy to learn and use stuff like TLA+. What fields do people find them useful in?

01HNNWZ0MV43FF 2y ago
I find my biggest problem is interfacing with apis from complex dependencies I can't control, usually OSes and gui libs. I assume there isn't a ton formal methods can do for that unless I set up a VM I can tightly control?
- buescher 2y ago
  At that point you're probably blowing up your verification/validation space to where it might be intractable , in both a machine and human sense. People have done research work in formal methods all the way down to the assembly level, of course, but could you even write the correctness properties for the software you're describing? Where you can use these methods - think of the part of your program's behavior you can describe with the article's "whiteboard" methods mentioned in the post above - truth tables, decision tables (! TIL), state machines/statecharts. If you can formulate it that way, not only is it easier to reason about and to test, but if you can also work out what would make it correct, you can run it through an automated checker.
Jtsummers 2y ago
My only time using TLA+ "in anger" was on an embedded system. There was a problem in the hardware portion and our boss wanted proof it was the hardware and not our software. He didn't accept any of our evidence that it was a hardware flaw, partially because our tests weren't failing 100% of the time. I used TLA+ and ended up with a handful of traces which we were able to recreate with the hardware and some small programs (remove everything our system actually did, just use the busted data bus) to demonstrate the failure, they always failed instead of failing only 90% of the time (shouldn't have been needed, it was obvious the hardware was broken). The TLA+ model started off being a reasonable fidelity model of the specified hardware bus, and then I started messing with it (in a deliberate fashion, altering state transitions) until I got traces and invariant violations similar to the real-world hardware. I've used Alloy for similar things, but only after the fact not during the investigation and as a way to learn Alloy. I'd use them both again (TLA+ especially) if I could convince people it was worth the time, but it can be difficult to get the time to spend on it at work while also meeting other work obligations. I've used TLA+ for some personal projects involving concurrent and distributed systems (toys, nothing notable just playing). I used TLA+ to demonstrate that my design worked as I intended, and then started writing code based on the model.

ChrisMarshallNY 2y ago

I worked for a [Japanese] corporation, that took “formal methods” into overdrive. They made really, really good hardware, but it was extremely painful for us software schlubs. That said, I don’t know if it’s really possible to do really big stuff, with a team, unless you have some degree of formality. Best practices are usually a good place to start, and I would suggest that the degree of necessary formality, is inversely proportional to the experience of the team. If you have a lot of really experienced engineers, in a mature team that has been together a long time, the formality is still there, but doesn’t need to be written down. I usually work alone, or as the sole technical person, in a diverse team. I’m really experienced, and don’t write much down. But I’m also really, really formal. It just doesn’t look like it.

jxramos 2y ago
Does it come out instead in PR reviews?
- ChrisMarshallNY 2y ago
  If I work alone, there aren’t any PRs. But I do spend a great deal of time reviewing my work; often going back, and tweaking and testing, for days. My testing code tends to dwarf my implementation code.
spankalee 2y ago
Formal methods is much more specific than formality and writing things down. There's a degree of proof that you achieve with formal methods that you don't even with design documents, reviews, and the usual tests.
- ChrisMarshallNY 2y ago
  Agreed, but also, “writing things down,” was a bit of a euphemism for the many, many aspects of a formal approach. The main issue is that we can get so wrapped up in the process, that we fail to get anything done. It’s a question of balance.
2y ago

erik_seaberg 2y ago

I learned some TLA+ and started reading about Coq, but I was pretty disappointed to learn of the "verification gap" between the the algorithm to be delivered in a normal programming language and the manually-restated algorithm that passed the checker. We need to make a checker's input language ergonomic enough for daily use and then "synthesize" something that runs efficiently while still being known correct, or make a checker understand everyday programs (which, not being so minimalist, probably have a much larger space of reachable states to check).

ukuina 2y ago
This is my biggest gripe with verification. I am hoping that LLMs help with inferring intent from a subroutine, then asking the programmer if the inferred intent is complete and correct, and then automatically writing/updating a verification harness.
- eschaton 2y ago
  What makes you think autocomplete on steroids with no internal reasoning capability or representation of knowledge would be at all useful for inferring intent? Or have you been fooled into thinking an LLM is something like Eurisko/Cyc?
  - pxeger1 2y ago
    Because ideally good code should make the intent obvious from the names and comments, so inferring a full description should really just be an autocomplete task.
    - eschaton 2y ago
      The topic is using an LLM to learn a codebase one doesn’t understand. Does that sound like a codebase that has names and comments from which a full description could be inferred?
  - bubblyworld 2y ago

kazinator 2y ago

Non-software engineering doesn't excessively use formal methods. Only where required. (Like where a system is tightly optimized.) For instance, in electronic engineering, you don't use the most accurate model of a diode at all times. Sometimes it's just a one-way valve. Sometimes, it's just one-way valve with a 0.7V drop (if silicon). In mass production, you will not get the accurate parts needed for the most formal model to be justifiable, and the cost of those parts would not be justified in most of the circuitry.

nanolith 2y ago

In my opinion, most developers should be using bounded model checking if available for their language / platform. This is certainly true for C, Rust, Java, and others. I consider bounded model checking to be "formal methods lite". It provides most of the benefits at a lower cost of entry than using a proof assistant or building constructive proofs. Really, there's little added overhead. Perhaps 30% to 40% more time to build out the function contracts and model checking. Given that this overhead more or less prevents errors that would likely be introduced without it, I think it's a reasonable investment. TLA+ is certainly related, since it uses an SMT solver at its base. I see it as useful for designing algorithms and protocols. A tool like CBMC or Kani provides similar guarantees at the source code level. It's not perfect, as currently CProver does not have direct threading support, but with a reasonable application of method shadowing and function contracts, even things like threading can be anticipated. Using a bounded model checker effectively means changing the design of software to work best with it. This is little different than using concepts like TDD or continuous integration.

vlovich123 2y ago
In my experience traditional property checks are pretty difficult to write already (30-40%). I get the sense that a bounded model check would be even more expensive than that, probably into the 2-3x range if not more. I’m talking about meaningfully complex logic, not very simple things.
- rtpg 2y ago
  It would be interesting to have a workbook of what people consider valuable examples of issues we are trying to solve. Like property checks are sometimes easy to write, when your property aligns well with property checking models! But then time-based stuff like TLA+ ends up working way better, sometimes. There are plenty of canonical examples out there for resolving some issues with types, and having a bunch of one-pagers on issues people hit that people might or might not want to tackle with some flavor of formal method.
- nanolith 2y ago
  You can write these checks as assertions in your regular source language. It's no more difficult than writing runtime parameter checks, really. There are some complexities, to be fair, but these are mostly around the performance of the model checker. Some things are easy to check, and other things, like loops and recursion, are harder to check. However, this is a matter of optimization, and with practice, this becomes quite easy to deal with.

Almondsetat 2y ago

In my opinion formal methods are what's missing from software engineering to make it a serious engineering discipline. In all other engineering fields you have to produce calculations and "proofs" that your design ought to work. In software engineering everything is basically overcomplicated handwaving.

atoav 2y ago
> In software engineering everything is basically overcomplicated handwaving. No, it is worse than that. There are people who claim the proof is the code itself. Just look at it. These are the same kind of people claiming good code needs no documentation. That is like a bridge engineer saying they need no structural calculation because the stability of the bridge is obvious to a certain kind of bridge nerd if they look at it. Only that civil engineers figured out after a few high profile bridge collapses that "trust me bro" isn't good enough and software engineering people are still in the: "trust him, he is a genius"-phase of the field.
- mrkeen 2y ago
  > There are people who claim the proof is the code itself. Yet this is what emerges when you write a sufficiently detailed proof. The more detail you add to your TLA+ model, the more it looks like just another implementation (albeit untyped, so it's pretty easy to slip errors into).
  - szundi 2y ago
    We should have a TLA+^2 then. Oh the complexity has to be expressed anyway? Uh Oh and users mostly rather suffer from bugs than give up complex desires and features? Uh We’re doomed haha
    - atoav 2y ago
      Isn't that why we have modularization? In the end you can formally verify low level stuff on a per module basis. Knowing that your PNG decoder is formally verified and therefore it is less likely that a user uploads a PNG and gets Runtime Code Execution within that process context isn't worth nothing. And if it allows attackers to get RCE the number of mysterious crashes it might have produced with weird PNGs is probably also non-zero. In the end all security measures are a layered effort and doing a bit formal verification, a bit unit testing, a bit fuzzing etc. is always better than mentally aiming for 100% and not doing anything at all. The question regarding formal verification is: What is the code that is running in the critical domain? Someone who writes safe code will try to minimize the amount of code/executables/complexity in that space. And that domain isn't necessarily a single process, it can be a part in the code, or a process until it dropped privileges etc. If all your code is critical domain it either means you failed to sanitize inputs, everything runs with yolo/root privileges, all of your customers share a single table in your database, your hardcoded admin password is 1234 — or maybe you write code that controls nuclear power plants, airplanes or similar things. But if it is the former, no amount of formal verification will save you anyways because wrote software like a money writes poems: By accident. If the idea of a critical domain is new to those reading this comment, if you never thought about user proviledges when writing an application, please read this as proof of the point that the field of software engineering still lacks in all sort of places and it is in all our interest, both professional and as users/potential victims to improve the situation.

DoingIsLearning 2y ago

Is there formal methods 'tooling' similar to TLA+ that is more targeted to State Machine design and perhaps State Machine Replication?

nradclif 2y ago
Model checking can be used to formally verify state machines. See https://en.wikipedia.org/wiki/Model_checking https://en.wikipedia.org/wiki/Model_checking.
hwayne 2y ago
https://p-org.github.io/P/ https://p-org.github.io/P/
rramadass 2y ago
See Tools section at https://en.wikipedia.org/wiki/Abstract_state_machine https://en.wikipedia.org/wiki/Abstract_state_machine

pjmlp 2y ago

The main issue is that most of these tools like TLA+, live in another dimension, proving something in TLA+, doesn't mean when the algorithm gets actually implemented in C, it still maps to TLA+ as proven. Formal methods need to be like SPARK 2014, or DbC, actually part of the programming language, or being able to generate code in the target language, interop with its libraries ecosystem, and have good quality good with performance, that won't make people want to remove the generated code and rewrite it manually.

pyrale 2y ago
For that you would need a proper, well-grounded type system and a language that doesn’t stray from it. Some fp languages are close enough to fit that bill; Rust too is going down this path: its type system was built to make a proof, after all.
IshKebab 2y ago
I don't know if that's always the case. My understanding is that TLA+ is really designed to prove properties about algorithms. Knowing that complex algorithms are correct is very useful eventually if it doesn't provide a correct implementation in a real world language. But TLA+ is a bit of an unusual proof language. I think most of them are like you describe: SPARK, Dafny, F*, CBMC, all the Rust ones, etc. I'm not sure about the interactive proof languages (Coq et al), they are too complicated for my normal sized brain.
- pjmlp 2y ago
  Yes, and making those languages (SPARK, Dafny, F*, CBMC,....) more widespread, the kind of something that everyone expects to be out of the box on their favourite language is how this can eventually gain more adoption, than a few selected companies, or academic research.
bvrmn 2y ago
TLA+ helps to find errors in your algorithm. It's a way easier than trying to model the algorithm in terms of end implementation. Too much complexity and state are introduced because of details.

verisimi 2y ago

> What is TLA+? > > TLA+ is a formal language for specifying systems used in industry and academia to verify complex distributed and concurrent systems. Among others, the TLA+ methodology is successfully applied at Amazon Web Services, Microsoft, and Oracle. https://conf.tlapl.us/home/ https://conf.tlapl.us/home/

hresvelgr 2y ago

I think we might potentially be looking at this backwards. There is a great talk by Jack Rusher [1] on why having really slow iteration loops and being too disconnected from running programs creates a desire for theorem proving because it becomes the faster way to arrive at a correct solution. I am of the belief that we need to return to modifying live environments instead of sending code through a lengthy build pipeline. Instead of trying to make live environments secure and durable we got scared and now we have modern CI/CD. [1] https://www.youtube.com/watch?v=8Ab3ArE8W3s https://www.youtube.com/watch?v=8Ab3ArE8W3s

yencabulator 2y ago
Good luck trying to get something like Paxos correct by poking at it in a REPL.
- hresvelgr 2y ago
  Not what I'm advocating and certainly not REPL. When I'm talking about a live environment, I mean something _like_ Pharo [1]. I'm arguing against long compile and deploy loops, not formal verification. [1] https://pharo.org/ https://pharo.org/

treprinum 2y ago

"Beware of bugs in the above code; I have only proved it correct, not tried it. " -- Donald Knuth

ozim 2y ago

Just wanted to post this video link in this discussion: Glenn Vanderburg - Real Software Engineering https://www.youtube.com/watch?v=RhdlBHHimeM https://www.youtube.com/watch?v=RhdlBHHimeM