12 ms·

Formal Methods: Just Good Engineering Practice? (2024)

211 points by aiono 2y ago

ot 2y ago
Previous discussion (Jun 2024): https://news.ycombinator.com/item?id=40753989 https://news.ycombinator.com/item?id=40753989
- aiono 2y ago
  Thanks, I couldn't find it via Google search on this website for some reason.
  - onionisafruit 2y ago
    I’m glad you couldn’t if that would have kept you from posting it today.
    - aiono 2y ago
      Yeah I wasn't going to post it if it was shared before. But I am happy that some are happy that it's reposted.
  - ot 2y ago
    Nothing wrong with reposts, it's just useful to link to previous discussions for context :)
  - ChrisArchitect 2y ago
    Google search? Use the HN search on site here: https://hn.algolia.com/?q=https%3A%2F%2Fbrooker.co.za%2Fblog%2F2024%2F04%2F17%2Fformal https://hn.algolia.com/?q=https%3A%2F%2Fbrooker.co.za%2Fblog...
- dang 2y ago
  Thanks! Macroexpanded: Formal methods: Just good engineering practice? - https://news.ycombinator.com/item?id=40753989 https://news.ycombinator.com/item?id=40753989 - June 2024 (149 comments) 15 Years of Formal Methods at AWS: Just Good Engineering Practice? - https://news.ycombinator.com/item?id=40283052 https://news.ycombinator.com/item?id=40283052 - May 2024 (1 comment)
franktankbank 2y ago
Too slow, planning==ossification any documentation can and will be used against you in the Agile court of law.
- intelVISA 2y ago
  Arguably, if 'real' Agile is ever found Formal Methods would be the antithesis of it: something provable and reproducible is blasphemy to True Believers.
  - AnimalMuppet 2y ago
    Not at all. Something that you can't easily change is terrifying. Reproducible? Sure, that's what unit tests are for. Make a change, prove that you didn't break any behavior that anybody relied on. But if you have to do a three-month-long formal proof run because the specification had a one-line change, then you're not agile, under any meaningful definition. (Where did three months come from? Thin air. I don't know how long a true formal proof would take. Depends on how many things you're proving, how long your spec is, and how much CPU power you have. I would think, though, to formally prove significant properties of a large code base would take a significant time.)
    - franktankbank 2y ago
      Sorry, we are discussing Agile not agile.
constantcrying 2y ago
Formal verification of software, as the article acknowledges, relies heavily on the type of software and the development process. To use formal verification you need to have formal requirements of the behavior of your software. Most software projects and design philosophies are simply incompatible with this. In software development and design can often fall together, but that means that it is uniquely ill suited for formal methods. If you are developing, before you are sure what you even want, then formal methods do not apply. But I agree that there are certain areas, mostly smaller, safety critical, systems, which rely on upfront specifications, which can heavily benefit from formal verification. E.g. Aerospace software relies heavily on verification.
- aiono 2y ago
  I think it's more formalisability than requiring upfront design. For example you may have an insurance claim automation system which you can't design upfront because most insurance providers have unspecified behaviour. But that doesn't mean you can refine your automation system as you get more information from interactions. You would still get the benefit that you ensure not leaving out any cases or not having any contradiction in your system
  - constantcrying 2y ago
    But that still relies on having a prior notion of the formal requirements of your system. I know little about insurance systems, but deriving a formal specification seems like a nightmare task. Although, as you mentioned, if you had a partial one you certainly would get some benefits from it.
    - aiono 2y ago
      It's been a while since I worked on those systems, but you usually decide on some rules that you refine over time. So they are purely logical decisions that you can formalize. I don't see why it would be hard to specify. I don't mean to specify all up front but one can specify the exact decision procedure that is implemented right now very easily in my experience. Generally you have a state machine representing the process. This state machine is usually embedded in the code, but code has a lot of noise around the state machine that makes it harder to see the underlying state machine.
commandlinefan 2y ago
I see this line of reasoning about formal methods a lot: software is big and complicated and hard to get right... therefore formal methods. On the one hand, I _want_ this to be true both for selfish and practical reasons: selfishly because I'm very very good at learning things that require an academic learning approach (read a book, work some exercises, practice) and if something I'm good at is important, that means more money for me. Practically because they're right, software _is_ big and complicated and hard to get right and as a practitioner, it's really frustrating when it does fail and I'm scrambling to figure out why. On the other hand, though, nobody ever seems to make a compelling case for how formal methods proposes to solve that problem. This author actually does better than most by pointing out how most modern "design" is a waste of time but doesn't really go into why TLA, say, is better than (demonstrably mostly useless) UML. There's sort of an implied suggestion that if you dedicate a few months (or years?) to learning TLA, you'll reach enlightenment and understand how it's helpful in a way that's impossible to articulate to the unenlightened. And that's not impossible to imagine! Calculus and Bayesian statistics are kind of like that; you need to really understand them before you can really see why they're useful. I always find myself left applying what I call "project manager" logic - I need to make a snap decision right now about whether or not I should invest time in this "formal method" stuff or not so I have to be observational: if it was really that helpful, more people would be applying it and the benefits would speak for themselves. They've been around a long, long time, though, and never caught on - it's hard not to conclude that there's probably a reason.
- hitchstory 2y ago
  >if it was really that helpful, more people would be applying it and the benefits would speak for themselves. They've been around a long, long time, though, and never caught on - it's hard not to conclude that there's probably a reason. My impression is that there are actually not that many business domains where a large investment in time and money to get domain logic correctness from 98% to 99.99% correct is actually called for. Formal methods are a large investment, too. No two ways around it. Also, while they havent really caught on in general, some of their ideas have made it into modern type systems.
  - 2y ago
thefaux 2y ago
Most of the articles I've read about formal methods feel like lead gen for consultants. That's fine but feels obnoxious when they implicitly act as though they have reached formal methods induced enlightenment that you can too if you buy a pack of trainings for your employees/coworkers or hire me as an employee to fix your bad (irresponsibly dangerous even!) programming habits. Get back to me when the formal methods actually generate high quality code that cannot deviate from the spec.
- erpellan 2y ago
  How about https://en.wikipedia.org/wiki/SPARK_(programming_language) https://en.wikipedia.org/wiki/SPARK_(programming_language)
  - lolinder 2y ago
    Ada is terminally underappreciated.
  - MaxBarraclough 2y ago
    Seconded. Regarding applying SPARK, the Tokeneer case-study is an interesting read. It's self-published by AdaCore. This summary page links to the full PDF: https://www.adacore.com/tokeneer https://www.adacore.com/tokeneer
- aiono 2y ago
  > Get back to me when the formal methods actually generate high quality code that cannot deviate from the spec That would be useful but there is a fundamental issue: code is too specific. İn formal specification you usually don't specify that detailed but you specify the general behaviour of the system. So usually the specification corresponds to a lot of programs with subtle differences. That's why code a documentation falls short: you don't know what is intentional and what is just a random choice. It's simply too specific to describe high level requirements. The other way around (verification of program with respect to the specification) can be more feasible to implement.
deleted 2y ago
[deleted]
deleted 2y ago
[deleted]
noelwelsh 2y ago
I would guess a majority of developers use formal methods these days. We just tend to call them type systems, and for some reason consider them a distinct category. If simulations count as formal methods, then tests, and particularly property-based testing, also make the cut.
jcgrillo 2y ago
The lightweight formal methods callout is a good one. Maintaining a suite of proptest[1] strategies alongside the codebase is not a very much larger investment than writing unit tests by hand, but the insights they provide due to extensive coverage and compact understandable failure cases are way better. And crucially this approach does align with normal software development practices. [1] https://crates.io/crates/proptest https://crates.io/crates/proptest
- andrepd 2y ago
  Yeah but proptest / qcheck is not formal methods at all. It's randomised testing.
  - jcgrillo 2y ago
    The assertion is that they're lightweight formal methods. Or is the article (and the proceedings of SOSP '21 it links to) wrong? EDIT: ah I see where there might be confusion--obviously a library for generating random test data and making assertions about code under test itself doesn't constitute anything like "formal methods" but the idea of using that library in the way described in the paper linked from the article does. But that's kinda always the thing about software libraries..
  - pfdietz 2y ago
    Property tests are informal tests of formal properties. They don't guarantee the properties hold, or that the formal properties are complete, but they exploit the existence of these formal properties. Once you have formal properties, you can write property-based tests using them, and I wonder how much of the benefit of formal methods could be obtained just by doing this. It's another example of using increased computing power (testing) to substitute for expensive hand labor (proving theorems). I'll also observe that even theorem proving systems benefit from a kind of property based testing. If there's a goal to prove the existence of a value satisfying some property, this is essentially a property based testing problem. Similarly, find a counterexample to a universally quantified formula (also an existential problem) can be used to prune off unproductive branches of a search tree.
trending486 2y ago
Modern formal methods like TLA+ and Alloy are as easy to pick up as Python, and other than having to write a spec (an ultra-simplified model of part of a system) they are completely automatic (based on model checkers). There is no reason for a modern software engineer not to have them on her radar. As a matter of fact most of the cloud systems you are using everyday have been verified with modern formal tools: Azure Cosmos DB, Dynamo DB, MongoDB, CockroachDB, ... and many others.
- tombert 2y ago
  I haven't done enough with Alloy to speak with any degree of competence with it, so I'll only speak on TLA+. While I do think TLA+ is relatively easy to pick up (especially compared to Isabelle or Coq), and I think it's pretty awesome, I'm hesitant to say it's as "easy to pick up as Python". You need a basic understanding of set theory and state machines to even get started, and more advanced concepts like algorithm refinement to get into the really useful juicy stuff. When I've tried to push TLA+ at work, the mathey syntax is usually a non-starter for most of my engineering colleagues. I don't think my coworkers are stupid by any stretch, but they are decidedly uninterested in re-learning any discrete math (if they ever learned it in the first place, which isn't a guarantee). For an engineer LARPing as an academic like me, TLA+'s notation isn't really hard at all, but I will often forget that most engineers only think in code.
  - Taikonerd 2y ago
    > When I've tried to push TLA+ at work, the mathey syntax is usually a non-starter Would they be interested in Quint?[0] If I understand correctly, Quint is very similar to TLA+, but with a more "code-looking" notation. And it has some nice dev tooling, like an LSP, which also lowers the barrier to entry. [0]: https://github.com/informalsystems/quint https://github.com/informalsystems/quint
    - tombert 2y ago
      Possible, I haven’t tried it. It’s still an uphill battle, because the comparison to unit tests always comes up, and I have to explain how they’re not equivalent.
AnimalMuppet 2y ago
Good engineering practice is to use the appropriate level of rigor. It depends on what the cost of failure is, and what the cost of the rigor is.
brap 2y ago
I’m not super experienced with formal verification, but I did dip my toes in it a few times. My impression is that it’s far from a magic bullet. Writing formal specs is basically like writing the code/tests just differently. And the more it covers the more it becomes the same thing. And it suffers from the same problems. My conclusion every time was that the code itself is the formal spec and the formal spec is the code. By analogy with construction, the code is both the building and the blueprint.
- davidmurdoch 2y ago
  This. In my very limited experience (i didn't write the code or specs), I've seen the runtime code find more bugs in the formal specs than the formal specs finding bugs in the runtime code.
- IshKebab 2y ago
  > My conclusion every time was that the code itself is the formal spec and the formal spec is the code. Yes you can end up with tautological specs, where it's more or less a copy of the code. E.g. you aren't going to benefit much from formally verifying `max()`. But there are many many cases where the formal specification is much much simpler and more obviously correct than the actual code. The classic examples are: * Any kind of encoding / decoding transformation has the property `decode(encode(x)) == x`. * Sorting: any sorting algorithm should result in a sorted array (forall i, j: i < j --> array[i] <= array[j])
  - ngruhn 2y ago
    I also think universal quantifiers ("for all ...") are a key distinguishing feature of specs. For example, a spec for a shortest path algorithm can be much simpler than any actual algorithm, largely because we can quantify over all (potentially infinitely many) paths: FORALL paths P from A to B: |shortestPath(A,B)| <= |P|
nimish 2y ago
Formal methods work great when the price of failure is absolute. Mostly pointless otherwise but can be a good exercise I guess.
- jillesvangurp 2y ago
  With most testing and verification, there's a law of diminishing returns. It helps you find stuff that you need to fix and there is always stuff to find. But at some point you've found enough of the stuff that needed fixing that you can use the software and it starts making money for you. Most people stop there. It's not going to make much more money if you continue your efforts and the risk of a lot of financial damage is usually not that high. A good software license will ensure that. You might be better off paying a decent lawyer than wasting time on formal methods. Lawyers aren't cheap. But neither is having your software engineering team faff about with a lot of complex tools for weeks on end. And with software you can just do an update if something is found later. Not a big deal usually. There are exceptions of course. With hardware things get more expensive. But still, judging from the state of e.g. most bluetooth and other hardware I've ever owned, the barrier of good enough is pretty low there too. Mostly things work and you can usually work around minor issues when they don't. Some, software justifies/requires going above and beyond doing testing. Especially if it controls critical hardware. I've never worked on such stuff. And even there the notion of releasing often and breaking stuff by testing it seems to be catching on. For example SpaceX is doing agile rocket development. They launch starship every few months until they get it reliable enough to launch things into orbit.
- aiono 2y ago
  I doubt that although I agree that it's much more useful when cost of a failure is higher. For example I work in a lab that formalizes requirements and we have real customers that pay us for formalization because they find it useful. Some products are things that a failure could cause injury or even possibly death. But not all systems have that high costs and they still see benefits.
synchronousq 2y ago
I just want to note, there exist two main flavors of formal methods: extrinsic techniques, which are disjoint from the code itself and generally reason about the specifications of code, and intrinsic techniques, which are inline with the code itself and reason about the code more directly. Historically, intrinsic techniques (such as type systems) reason about code at a functional level, while extrinsic techniques (such as decidable model checkers like Spin/P) reason about a model of the code, ascribed to formalism like an automata. But imo we're currently in a complete golden age of formal methods research, and extrinsic techniques are falling out of flavor in comparison to intrinsic methods as pushed by type system advancements and projects like Verus [1]. [1] https://github.com/verus-lang/verus https://github.com/verus-lang/verus
- hashxyz 2y ago
  I don’t see how the distinction makes any sense when the Verus project you linked requires you to write correctness specs. It sounded like intrinsic techniques were preferred because they would not require you to write and maintain a separate spec, but this is not the case.
  - lolinder 2y ago
    I prefer intrinsic techniques because it prevents the model from being out of sync with the implementation. The thing that's never made any sense to me about using a marble checker for anything but concurrency issues (which are hard enough to warrant it) is that once you've validated your model you have to go actually implement it, and that's usually the most error prone part of the process. If the correctness spec has to be written manually but prevents you from diverging from the spec in your implementation, that's a huge step up from extrinsic model checkers.
    - ad_hockey 2y ago
      Lamport's rationale is that after an architect designs a building, the builders may still put electrical sockets in the wrong place and make other mistakes. But that's not a reason to start construction without a plan at all.
begueradj 2y ago
For those interested in the information exchange about this same article: https://news.ycombinator.com/item?id=40753989 https://news.ycombinator.com/item?id=40753989
markusde 2y ago
I'd recommend anyone with a passing interest in the role formal techniques can play in software development watch this [1] talk. Mike Dodds is a principal scientist at Galois (a company which has a lot of experience with applying formal methods in industry and government) and the talk does a good job at explaining where they've seen value-added from formal methods, and the right kind of formal methods for different applications. [1]: https://www.youtube.com/watch?v=gfvvowAc130 https://www.youtube.com/watch?v=gfvvowAc130
Animats 2y ago
The article is thin on specifics. Some problems specify well. A database is an example. A spec for a database can be written in terms of exhaustive search, running the query against everything. Now show that an efficient database yields the same output.
IshKebab 2y ago
IMO formal software verification is still waaay too difficult to be worth it in all but the most extreme cases. That's really different to formal hardware verification where it is a no-brainer. I keep trying to learn it, but you need to be a real expert. Like "I wrote the compiler" level expert for most systems. For example I tried to prove a varint encoder/decoder. It worked for one or two bytes, but not more. Asking for help the reason was that the compiler internally only unrolls loops 5 times, or some random internal detail like that that you could never really hope to know. I've been learning Lean recently, and ... I mean I like it, but if you learn it you're going to encounter documentation like this: > Definitional equality includes η-equivalence of functions and single-constructor inductive types. That is, fun x => f x is definitionally equal to f, and S.mk x.f1 x.f2 is definitionally equal to x, if S is a structure with fields f1 and f2. It also features proof irrelevance, so any two proofs of the same proposition are definitionally equal. It is reflexive, symmetric, and a congruence. And that's not really a knock on Lean - it seems to have some of the better documentation out of the alternatives.
- aiono 2y ago
  > And that's not really a knock on Lean - it seems to have some of the better documentation out of the alternatives. It looks scary but actually all those concepts are really simple and probably things you are already familiar with.
- jayaprabhakar 2y ago
  Have you tried FizzBee.io? It has a python-like syntax. Take a look at the example. https://fizzbee.io/examples/two_phase_commit_actors/#complete-code https://fizzbee.io/examples/two_phase_commit_actors/#complet... Formal methods don't have to be complex. The issue is, most formal methods are designed as an academic exercise to demonstrate a specific topic the professor was interested in. (Or TLA+, that was designed specifically for writing papers)
charleshn 2y ago
On lightweight formal methods, a favorite of mine that's not widely known is trace verification using Linear Temporal Logic [0]. Basically you just need to log events - which you can even have for free in event-driven architectures etc - and run some predicates on execution traces, e.g. "Always(Locked, Implies(Eventually(Unlocked)))", etc. One can run it on historical traces, but also couple it to stress tests, fuzzing etc to explore the state space. Quite simple, powerful and widely applicable, and doesn't require a model, just predicates. [0] https://en.m.wikipedia.org/wiki/Linear_temporal_logic https://en.m.wikipedia.org/wiki/Linear_temporal_logic
- johnbender 2y ago
  A minor point. This is more akin to testing because you’re only checking your formulae against a subset of system traces. Formal methods connotes comprehensive evidence about system behavior. In the case of TLA and similar system that’s a state machine and not the real system but the output for the state machine is a proof that your LTL/CTL/TLA properties hold for all behaviors of the system (traces or trees of traces).
  - charleshn 2y ago
    Definitely, I'm playing fast and loose with "lightweight formal method here", thanks for making it clear. I was mentioning it in the same context as e.g. the Amazon paper on lightweight formal methods [0] where they use property-based testing to test that the implementation conforms to the model specification. In a similar spirit, linearizability checkers like Porcupine [1] are a nice mix of formalism and usability. I really like those because they are incredibly powerful, don't require a model and verify the actual implementation - obviously as you mention they are not exhaustive. [0] https://assets.amazon.science/77/5e/4a7c238f4ce890efdc325df83263/using-lightweight-formal-methods-to-validate-a-key-value-storage-node-in-amazon-s3-2.pdf https://assets.amazon.science/77/5e/4a7c238f4ce890efdc325df8... [1] https://github.com/anishathalye/porcupine https://github.com/anishathalye/porcupine
UltraSane 2y ago
AWS has said that when software has a robust set of formal verification tests they can be very aggressive when optimizing it and be confident that they aren't changing its behavior. They say they were able to optimize their IAM authentication code by over 50% this way.
linkerdoo 2y ago
[dead]
lincpa 2y ago
[dead]
jgalt212 2y ago
If a TLA+ transpiler could emit Python, Javascript, Java, C, Rust, C++, Go (even just one of these), it would be infinitely more usable in that it helps you cross the gap from "I know my TLA+ is correct" to "I know my Go is correct". Or as a baby step, does TLA+ emit comprehensive test cases? Then we as programmers still have to do the hand transpilation step, but at least we can be assured our implementation is correct (if not efficient).
jayaprabhakar 2y ago
One issue with the current proponents of formal methods is, they want to claim others who don't use formal methods as "lazy" or "dumb" and want to claim their superiority because they "do the right thing" and "mastered a complex language". Some of them (not all, I know a few good ones) are, actually one trick pony. For example, ask them about other formal methods systems they learnt or tried in the recent years, they would claim they are "too busy" to learn anything new. Recent easier to use formal methods: 1. FizzBee (Uses Python dialect, almost reads like pseudo code) 2. Quint: Another formal language with easier to use syntax 3. P: Use syntax similar to C# users. The author of the posted article himself posted another article that Formal methods solves only half his problems (https://brooker.co.za/blog/2022/06/02/formal.html https://brooker.co.za/blog/2022/06/02/formal.html) But the problem he mentioned is actually solved by PRISM (It is not new). But Brooker just won'd bother to look around or learn.

211 points by aiono 2y ago

ot 2y ago

Previous discussion (Jun 2024): https://news.ycombinator.com/item?id=40753989 https://news.ycombinator.com/item?id=40753989

aiono 2y ago
Thanks, I couldn't find it via Google search on this website for some reason.
- onionisafruit 2y ago
  I’m glad you couldn’t if that would have kept you from posting it today.
  - aiono 2y ago
    Yeah I wasn't going to post it if it was shared before. But I am happy that some are happy that it's reposted.
- ot 2y ago
  Nothing wrong with reposts, it's just useful to link to previous discussions for context :)
- ChrisArchitect 2y ago
  Google search? Use the HN search on site here: https://hn.algolia.com/?q=https%3A%2F%2Fbrooker.co.za%2Fblog%2F2024%2F04%2F17%2Fformal https://hn.algolia.com/?q=https%3A%2F%2Fbrooker.co.za%2Fblog...
dang 2y ago
Thanks! Macroexpanded: Formal methods: Just good engineering practice? - https://news.ycombinator.com/item?id=40753989 https://news.ycombinator.com/item?id=40753989 - June 2024 (149 comments) 15 Years of Formal Methods at AWS: Just Good Engineering Practice? - https://news.ycombinator.com/item?id=40283052 https://news.ycombinator.com/item?id=40283052 - May 2024 (1 comment)

franktankbank 2y ago

Too slow, planning==ossification any documentation can and will be used against you in the Agile court of law.

intelVISA 2y ago
Arguably, if 'real' Agile is ever found Formal Methods would be the antithesis of it: something provable and reproducible is blasphemy to True Believers.
- AnimalMuppet 2y ago
  Not at all. Something that you can't easily change is terrifying. Reproducible? Sure, that's what unit tests are for. Make a change, prove that you didn't break any behavior that anybody relied on. But if you have to do a three-month-long formal proof run because the specification had a one-line change, then you're not agile, under any meaningful definition. (Where did three months come from? Thin air. I don't know how long a true formal proof would take. Depends on how many things you're proving, how long your spec is, and how much CPU power you have. I would think, though, to formally prove significant properties of a large code base would take a significant time.)
  - franktankbank 2y ago
    Sorry, we are discussing Agile not agile.

constantcrying 2y ago

Formal verification of software, as the article acknowledges, relies heavily on the type of software and the development process. To use formal verification you need to have formal requirements of the behavior of your software. Most software projects and design philosophies are simply incompatible with this. In software development and design can often fall together, but that means that it is uniquely ill suited for formal methods. If you are developing, before you are sure what you even want, then formal methods do not apply. But I agree that there are certain areas, mostly smaller, safety critical, systems, which rely on upfront specifications, which can heavily benefit from formal verification. E.g. Aerospace software relies heavily on verification.

aiono 2y ago
I think it's more formalisability than requiring upfront design. For example you may have an insurance claim automation system which you can't design upfront because most insurance providers have unspecified behaviour. But that doesn't mean you can refine your automation system as you get more information from interactions. You would still get the benefit that you ensure not leaving out any cases or not having any contradiction in your system
- constantcrying 2y ago
  But that still relies on having a prior notion of the formal requirements of your system. I know little about insurance systems, but deriving a formal specification seems like a nightmare task. Although, as you mentioned, if you had a partial one you certainly would get some benefits from it.
  - aiono 2y ago
    It's been a while since I worked on those systems, but you usually decide on some rules that you refine over time. So they are purely logical decisions that you can formalize. I don't see why it would be hard to specify. I don't mean to specify all up front but one can specify the exact decision procedure that is implemented right now very easily in my experience. Generally you have a state machine representing the process. This state machine is usually embedded in the code, but code has a lot of noise around the state machine that makes it harder to see the underlying state machine.

commandlinefan 2y ago

I see this line of reasoning about formal methods a lot: software is big and complicated and hard to get right... therefore formal methods. On the one hand, I _want_ this to be true both for selfish and practical reasons: selfishly because I'm very very good at learning things that require an academic learning approach (read a book, work some exercises, practice) and if something I'm good at is important, that means more money for me. Practically because they're right, software _is_ big and complicated and hard to get right and as a practitioner, it's really frustrating when it does fail and I'm scrambling to figure out why. On the other hand, though, nobody ever seems to make a compelling case for how formal methods proposes to solve that problem. This author actually does better than most by pointing out how most modern "design" is a waste of time but doesn't really go into why TLA, say, is better than (demonstrably mostly useless) UML. There's sort of an implied suggestion that if you dedicate a few months (or years?) to learning TLA, you'll reach enlightenment and understand how it's helpful in a way that's impossible to articulate to the unenlightened. And that's not impossible to imagine! Calculus and Bayesian statistics are kind of like that; you need to really understand them before you can really see why they're useful. I always find myself left applying what I call "project manager" logic - I need to make a snap decision right now about whether or not I should invest time in this "formal method" stuff or not so I have to be observational: if it was really that helpful, more people would be applying it and the benefits would speak for themselves. They've been around a long, long time, though, and never caught on - it's hard not to conclude that there's probably a reason.

hitchstory 2y ago
>if it was really that helpful, more people would be applying it and the benefits would speak for themselves. They've been around a long, long time, though, and never caught on - it's hard not to conclude that there's probably a reason. My impression is that there are actually not that many business domains where a large investment in time and money to get domain logic correctness from 98% to 99.99% correct is actually called for. Formal methods are a large investment, too. No two ways around it. Also, while they havent really caught on in general, some of their ideas have made it into modern type systems.
- 2y ago

thefaux 2y ago

Most of the articles I've read about formal methods feel like lead gen for consultants. That's fine but feels obnoxious when they implicitly act as though they have reached formal methods induced enlightenment that you can too if you buy a pack of trainings for your employees/coworkers or hire me as an employee to fix your bad (irresponsibly dangerous even!) programming habits. Get back to me when the formal methods actually generate high quality code that cannot deviate from the spec.

erpellan 2y ago
How about https://en.wikipedia.org/wiki/SPARK_(programming_language) https://en.wikipedia.org/wiki/SPARK_(programming_language)
- lolinder 2y ago
  Ada is terminally underappreciated.
- MaxBarraclough 2y ago
  Seconded. Regarding applying SPARK, the Tokeneer case-study is an interesting read. It's self-published by AdaCore. This summary page links to the full PDF: https://www.adacore.com/tokeneer https://www.adacore.com/tokeneer
aiono 2y ago
> Get back to me when the formal methods actually generate high quality code that cannot deviate from the spec That would be useful but there is a fundamental issue: code is too specific. İn formal specification you usually don't specify that detailed but you specify the general behaviour of the system. So usually the specification corresponds to a lot of programs with subtle differences. That's why code a documentation falls short: you don't know what is intentional and what is just a random choice. It's simply too specific to describe high level requirements. The other way around (verification of program with respect to the specification) can be more feasible to implement.

deleted 2y ago

[deleted]

deleted 2y ago

[deleted]

noelwelsh 2y ago

I would guess a majority of developers use formal methods these days. We just tend to call them type systems, and for some reason consider them a distinct category. If simulations count as formal methods, then tests, and particularly property-based testing, also make the cut.

jcgrillo 2y ago

The lightweight formal methods callout is a good one. Maintaining a suite of proptest[1] strategies alongside the codebase is not a very much larger investment than writing unit tests by hand, but the insights they provide due to extensive coverage and compact understandable failure cases are way better. And crucially this approach does align with normal software development practices. [1] https://crates.io/crates/proptest https://crates.io/crates/proptest

andrepd 2y ago
Yeah but proptest / qcheck is not formal methods at all. It's randomised testing.
- jcgrillo 2y ago
  The assertion is that they're lightweight formal methods. Or is the article (and the proceedings of SOSP '21 it links to) wrong? EDIT: ah I see where there might be confusion--obviously a library for generating random test data and making assertions about code under test itself doesn't constitute anything like "formal methods" but the idea of using that library in the way described in the paper linked from the article does. But that's kinda always the thing about software libraries..
- pfdietz 2y ago
  Property tests are informal tests of formal properties. They don't guarantee the properties hold, or that the formal properties are complete, but they exploit the existence of these formal properties. Once you have formal properties, you can write property-based tests using them, and I wonder how much of the benefit of formal methods could be obtained just by doing this. It's another example of using increased computing power (testing) to substitute for expensive hand labor (proving theorems). I'll also observe that even theorem proving systems benefit from a kind of property based testing. If there's a goal to prove the existence of a value satisfying some property, this is essentially a property based testing problem. Similarly, find a counterexample to a universally quantified formula (also an existential problem) can be used to prune off unproductive branches of a search tree.

trending486 2y ago

Modern formal methods like TLA+ and Alloy are as easy to pick up as Python, and other than having to write a spec (an ultra-simplified model of part of a system) they are completely automatic (based on model checkers). There is no reason for a modern software engineer not to have them on her radar. As a matter of fact most of the cloud systems you are using everyday have been verified with modern formal tools: Azure Cosmos DB, Dynamo DB, MongoDB, CockroachDB, ... and many others.

tombert 2y ago
I haven't done enough with Alloy to speak with any degree of competence with it, so I'll only speak on TLA+. While I do think TLA+ is relatively easy to pick up (especially compared to Isabelle or Coq), and I think it's pretty awesome, I'm hesitant to say it's as "easy to pick up as Python". You need a basic understanding of set theory and state machines to even get started, and more advanced concepts like algorithm refinement to get into the really useful juicy stuff. When I've tried to push TLA+ at work, the mathey syntax is usually a non-starter for most of my engineering colleagues. I don't think my coworkers are stupid by any stretch, but they are decidedly uninterested in re-learning any discrete math (if they ever learned it in the first place, which isn't a guarantee). For an engineer LARPing as an academic like me, TLA+'s notation isn't really hard at all, but I will often forget that most engineers only think in code.
- Taikonerd 2y ago
  > When I've tried to push TLA+ at work, the mathey syntax is usually a non-starter Would they be interested in Quint?[0] If I understand correctly, Quint is very similar to TLA+, but with a more "code-looking" notation. And it has some nice dev tooling, like an LSP, which also lowers the barrier to entry. [0]: https://github.com/informalsystems/quint https://github.com/informalsystems/quint
  - tombert 2y ago
    Possible, I haven’t tried it. It’s still an uphill battle, because the comparison to unit tests always comes up, and I have to explain how they’re not equivalent.

AnimalMuppet 2y ago

Good engineering practice is to use the appropriate level of rigor. It depends on what the cost of failure is, and what the cost of the rigor is.

brap 2y ago

I’m not super experienced with formal verification, but I did dip my toes in it a few times. My impression is that it’s far from a magic bullet. Writing formal specs is basically like writing the code/tests just differently. And the more it covers the more it becomes the same thing. And it suffers from the same problems. My conclusion every time was that the code itself is the formal spec and the formal spec is the code. By analogy with construction, the code is both the building and the blueprint.

davidmurdoch 2y ago
This. In my very limited experience (i didn't write the code or specs), I've seen the runtime code find more bugs in the formal specs than the formal specs finding bugs in the runtime code.
IshKebab 2y ago
> My conclusion every time was that the code itself is the formal spec and the formal spec is the code. Yes you can end up with tautological specs, where it's more or less a copy of the code. E.g. you aren't going to benefit much from formally verifying `max()`. But there are many many cases where the formal specification is much much simpler and more obviously correct than the actual code. The classic examples are: * Any kind of encoding / decoding transformation has the property `decode(encode(x)) == x`. * Sorting: any sorting algorithm should result in a sorted array (forall i, j: i < j --> array[i] <= array[j])
- ngruhn 2y ago
  I also think universal quantifiers ("for all ...") are a key distinguishing feature of specs. For example, a spec for a shortest path algorithm can be much simpler than any actual algorithm, largely because we can quantify over all (potentially infinitely many) paths: FORALL paths P from A to B: |shortestPath(A,B)| <= |P|

nimish 2y ago

Formal methods work great when the price of failure is absolute. Mostly pointless otherwise but can be a good exercise I guess.

jillesvangurp 2y ago
With most testing and verification, there's a law of diminishing returns. It helps you find stuff that you need to fix and there is always stuff to find. But at some point you've found enough of the stuff that needed fixing that you can use the software and it starts making money for you. Most people stop there. It's not going to make much more money if you continue your efforts and the risk of a lot of financial damage is usually not that high. A good software license will ensure that. You might be better off paying a decent lawyer than wasting time on formal methods. Lawyers aren't cheap. But neither is having your software engineering team faff about with a lot of complex tools for weeks on end. And with software you can just do an update if something is found later. Not a big deal usually. There are exceptions of course. With hardware things get more expensive. But still, judging from the state of e.g. most bluetooth and other hardware I've ever owned, the barrier of good enough is pretty low there too. Mostly things work and you can usually work around minor issues when they don't. Some, software justifies/requires going above and beyond doing testing. Especially if it controls critical hardware. I've never worked on such stuff. And even there the notion of releasing often and breaking stuff by testing it seems to be catching on. For example SpaceX is doing agile rocket development. They launch starship every few months until they get it reliable enough to launch things into orbit.
aiono 2y ago
I doubt that although I agree that it's much more useful when cost of a failure is higher. For example I work in a lab that formalizes requirements and we have real customers that pay us for formalization because they find it useful. Some products are things that a failure could cause injury or even possibly death. But not all systems have that high costs and they still see benefits.

synchronousq 2y ago

I just want to note, there exist two main flavors of formal methods: extrinsic techniques, which are disjoint from the code itself and generally reason about the specifications of code, and intrinsic techniques, which are inline with the code itself and reason about the code more directly. Historically, intrinsic techniques (such as type systems) reason about code at a functional level, while extrinsic techniques (such as decidable model checkers like Spin/P) reason about a model of the code, ascribed to formalism like an automata. But imo we're currently in a complete golden age of formal methods research, and extrinsic techniques are falling out of flavor in comparison to intrinsic methods as pushed by type system advancements and projects like Verus [1]. [1] https://github.com/verus-lang/verus https://github.com/verus-lang/verus

hashxyz 2y ago
I don’t see how the distinction makes any sense when the Verus project you linked requires you to write correctness specs. It sounded like intrinsic techniques were preferred because they would not require you to write and maintain a separate spec, but this is not the case.
- lolinder 2y ago
  I prefer intrinsic techniques because it prevents the model from being out of sync with the implementation. The thing that's never made any sense to me about using a marble checker for anything but concurrency issues (which are hard enough to warrant it) is that once you've validated your model you have to go actually implement it, and that's usually the most error prone part of the process. If the correctness spec has to be written manually but prevents you from diverging from the spec in your implementation, that's a huge step up from extrinsic model checkers.
  - ad_hockey 2y ago
    Lamport's rationale is that after an architect designs a building, the builders may still put electrical sockets in the wrong place and make other mistakes. But that's not a reason to start construction without a plan at all.

begueradj 2y ago

For those interested in the information exchange about this same article: https://news.ycombinator.com/item?id=40753989 https://news.ycombinator.com/item?id=40753989

markusde 2y ago

I'd recommend anyone with a passing interest in the role formal techniques can play in software development watch this [1] talk. Mike Dodds is a principal scientist at Galois (a company which has a lot of experience with applying formal methods in industry and government) and the talk does a good job at explaining where they've seen value-added from formal methods, and the right kind of formal methods for different applications. [1]: https://www.youtube.com/watch?v=gfvvowAc130 https://www.youtube.com/watch?v=gfvvowAc130

Animats 2y ago

The article is thin on specifics. Some problems specify well. A database is an example. A spec for a database can be written in terms of exhaustive search, running the query against everything. Now show that an efficient database yields the same output.

IshKebab 2y ago

IMO formal software verification is still waaay too difficult to be worth it in all but the most extreme cases. That's really different to formal hardware verification where it is a no-brainer. I keep trying to learn it, but you need to be a real expert. Like "I wrote the compiler" level expert for most systems. For example I tried to prove a varint encoder/decoder. It worked for one or two bytes, but not more. Asking for help the reason was that the compiler internally only unrolls loops 5 times, or some random internal detail like that that you could never really hope to know. I've been learning Lean recently, and ... I mean I like it, but if you learn it you're going to encounter documentation like this: > Definitional equality includes η-equivalence of functions and single-constructor inductive types. That is, fun x => f x is definitionally equal to f, and S.mk x.f1 x.f2 is definitionally equal to x, if S is a structure with fields f1 and f2. It also features proof irrelevance, so any two proofs of the same proposition are definitionally equal. It is reflexive, symmetric, and a congruence. And that's not really a knock on Lean - it seems to have some of the better documentation out of the alternatives.

aiono 2y ago
> And that's not really a knock on Lean - it seems to have some of the better documentation out of the alternatives. It looks scary but actually all those concepts are really simple and probably things you are already familiar with.
jayaprabhakar 2y ago
Have you tried FizzBee.io? It has a python-like syntax. Take a look at the example. https://fizzbee.io/examples/two_phase_commit_actors/#complete-code https://fizzbee.io/examples/two_phase_commit_actors/#complet... Formal methods don't have to be complex. The issue is, most formal methods are designed as an academic exercise to demonstrate a specific topic the professor was interested in. (Or TLA+, that was designed specifically for writing papers)

charleshn 2y ago

On lightweight formal methods, a favorite of mine that's not widely known is trace verification using Linear Temporal Logic [0]. Basically you just need to log events - which you can even have for free in event-driven architectures etc - and run some predicates on execution traces, e.g. "Always(Locked, Implies(Eventually(Unlocked)))", etc. One can run it on historical traces, but also couple it to stress tests, fuzzing etc to explore the state space. Quite simple, powerful and widely applicable, and doesn't require a model, just predicates. [0] https://en.m.wikipedia.org/wiki/Linear_temporal_logic https://en.m.wikipedia.org/wiki/Linear_temporal_logic

johnbender 2y ago
A minor point. This is more akin to testing because you’re only checking your formulae against a subset of system traces. Formal methods connotes comprehensive evidence about system behavior. In the case of TLA and similar system that’s a state machine and not the real system but the output for the state machine is a proof that your LTL/CTL/TLA properties hold for all behaviors of the system (traces or trees of traces).
- charleshn 2y ago
  Definitely, I'm playing fast and loose with "lightweight formal method here", thanks for making it clear. I was mentioning it in the same context as e.g. the Amazon paper on lightweight formal methods [0] where they use property-based testing to test that the implementation conforms to the model specification. In a similar spirit, linearizability checkers like Porcupine [1] are a nice mix of formalism and usability. I really like those because they are incredibly powerful, don't require a model and verify the actual implementation - obviously as you mention they are not exhaustive. [0] https://assets.amazon.science/77/5e/4a7c238f4ce890efdc325df83263/using-lightweight-formal-methods-to-validate-a-key-value-storage-node-in-amazon-s3-2.pdf https://assets.amazon.science/77/5e/4a7c238f4ce890efdc325df8... [1] https://github.com/anishathalye/porcupine https://github.com/anishathalye/porcupine

UltraSane 2y ago

AWS has said that when software has a robust set of formal verification tests they can be very aggressive when optimizing it and be confident that they aren't changing its behavior. They say they were able to optimize their IAM authentication code by over 50% this way.

linkerdoo 2y ago

[dead]

lincpa 2y ago

[dead]

jgalt212 2y ago

If a TLA+ transpiler could emit Python, Javascript, Java, C, Rust, C++, Go (even just one of these), it would be infinitely more usable in that it helps you cross the gap from "I know my TLA+ is correct" to "I know my Go is correct". Or as a baby step, does TLA+ emit comprehensive test cases? Then we as programmers still have to do the hand transpilation step, but at least we can be assured our implementation is correct (if not efficient).

jayaprabhakar 2y ago

One issue with the current proponents of formal methods is, they want to claim others who don't use formal methods as "lazy" or "dumb" and want to claim their superiority because they "do the right thing" and "mastered a complex language". Some of them (not all, I know a few good ones) are, actually one trick pony. For example, ask them about other formal methods systems they learnt or tried in the recent years, they would claim they are "too busy" to learn anything new. Recent easier to use formal methods: 1. FizzBee (Uses Python dialect, almost reads like pseudo code) 2. Quint: Another formal language with easier to use syntax 3. P: Use syntax similar to C# users. The author of the posted article himself posted another article that Formal methods solves only half his problems (https://brooker.co.za/blog/2022/06/02/formal.html https://brooker.co.za/blog/2022/06/02/formal.html) But the problem he mentioned is actually solved by PRISM (It is not new). But Brooker just won'd bother to look around or learn.