5 ms·
I think the cost of some formal methods have long been over-stated. Model checking, for example, is not as hard as it sounds and not nearly as expensive or tim
by agentultra 1y ago
I think the cost of some formal methods have long been over-stated.
Model checking, for example, is not as hard as it sounds and not nearly as expensive or time consuming as building the wrong thing. Most programmers I’ve taught don’t seem to have too much difficulty learning TLA+ or Alloy. The concepts themselves are fundamentally rather simple.
Theorem proving does take some expertise. But it’s also not an insurmountable obstacle.
However I agree that there’s a spectrum of cost and the higher you go down the assurance chain the effort and time it will take. Often we do price in the cost of errors into the holistic process of software (eg: SRE style error budgets, iterative development, etc).
One angle that works for me when deciding when to use a more substantial FM is the cost of getting it wrong (or conversely, how important is it that we get some key thing right)?
If I’m building a financial database can my business afford to lose customers’ money? Do we have that liability built into our insurance?
Sometimes you need to go slow at first in order to go fast later.
And some properties are simply too hard to trust to some boxes and arrows and a prayer.
- almostgotcaught 1y ago> I think the cost of some formal methods have long been over-stated. how are you measuring cost? the cost of anything in this space (or any other rarefied space) is the cost a "principal/staff" (maybe 1-person year) to build it and then a team of very very strong seniors to maintain it. who can afford that? > Most programmers I’ve taught don’t seem to have too much difficulty learning TLA+ or Alloy. The concepts themselves are fundamentally rather simple. this is like saying building a prod LLM pipeline is no big deal because learning the basics of pytorch is easy. more relevantly: what are "most programmers" going to do when they hit an undecidable clause? here's a razor for highly technical projects (a kind of efficient market hypothesis for software if you will): if it's easy to do then it's worthless (highly-commofidied, marginal value, etc.).
- bravesoul2 1y agoFormal methods can be understood by interns. This is the weird thing about this industry. Make people run gauntlets then label them and tie their hands behind their backs. Formal methods is just another tool. Do you need a principal engineer with 15yoe for Haskell or Rust code. In today's AI and low head count world you want someone who is really good at that thing (regardless of experience) Needing a principal who can go deep on Kafka queues in a design interview isn't what is required. Most organisations are measuring impact narratives not skill to get up the org chart.
- YetAnotherNick 1y agoI don't know which interns are you talking to. Most interns can hardly understand e.g. say what `useEffect` means, let alone would be able to understand how to model it.
- bravesoul2 1y agoOnes that studied CS and got a good grade. Formal systems may be easier than React to understand (assuming decent effort put into both) as there is more of a disciplined teaching culture around it. useEffect is a feature of a framework React made by a tech company, with coders taking the mantle of teaching it to others. I'm not joking.
- creata 1y ago> Formal systems may be easier than React to understand Some specific formal systems, maybe. I feel like a lot of people could get some mileage out of learning Dafny, and it'd definitely be easier than learning React imo.
- bubblyworld 1y agoGo write something simple like a merge-sort with formal guarantees in Dafny, and tell me it's easier than working on a react project afterwards =P
- creata 1y agoMerge sort in Dafny: predicate sorted(a: seq<int>) { forall i, j :: 0 <= i <= j < |a| ==> a[i] <= a[j] } predicate merge_invariants(a: seq<int>, b: seq<int>, c: array<int>, i: nat, j: nat) reads c { && i <= |a| && j <= |b| && i + j <= c.Length && multiset(c[..i+j]) == multiset(a[..i]) + multiset(b[..j]) && (forall k1, k2 :: 0 <= k1 < i && j <= k2 < |b| ==> a[k1] <= b[k2]) && (forall k1, k2 :: 0 <= k1 < j && i <= k2 < |a| ==> b[k1] <= a[k2]) && sorted(c[..i+j]) && (forall k1, k2 :: 0 <= k1 < i + j && j <= k2 < |b| ==> c[k1] <= b[k2]) && (forall k1, k2 :: 0 <= k1 < i + j && i <= k2 < |a| ==> c[k1] <= a[k2]) } method merge(a: seq<int>, b: seq<int>) returns (out: seq<int>) requires sorted(a) requires sorted(b) ensures multiset(a) + multiset(b) == multiset(out) ensures sorted(out) { var i := 0; var j := 0; var c := new int[|a| + |b|]; while i < |a| && j < |b| decreases |a| + |b| - (i + j) invariant merge_invariants(a, b, c, i, j) { assert a[..i+1] == a[..i] + [a[i]]; assert b[..j+1] == b[..j] + [b[j]]; if a[i] <= b[j] { c[i + j] := a[i]; i := i + 1; } else { c[i + j] := b[j]; j := j + 1; } } while i < |a| invariant merge_invariants(a, b, c, i, j) { assert a[..i+1] == a[..i] + [a[i]]; c[i + j] := a[i]; i := i + 1; } while j < |b| invariant merge_invariants(a, b, c, i, j) { assert b[..j+1] == b[..j] + [b[j]]; c[i + j] := b[j]; j := j + 1; } assert a[..i] == a; assert b[..j] == b; assert c[..i+j] == c[..]; return c[..]; } method merge_sort(a: seq<int>) returns (out: seq<int>) decreases |a| ensures multiset(out) == multiset(a) ensures sorted(out) { if |a| <= 1 { assert sorted(a); out := a; } else { var half := |a| / 2; assert a[..half] + a[half..] == a; var l := merge_sort(a[..half]); var r := merge_sort(a[half..]); out := merge(l, r); } } Imo it's a lot easier to explain than React. Preconditions, postconditions, loop invariants, assertions, termination arguments, and... that's about it, right?
- g9yuayon 1y agoSpecifying a system correctly can be hard with the previous generation of tools. For instance, using LTL to describe system properties is not necessarily easy. I remember there used to be pattern library for model checking or for temporal logic. For something as simple as checking bounded existence, one has to write LTL formula like below. That certainly is out of most people's interest. Fortunately tools have improved a lot, and engineers do not really need to study temporal logic deeply for many cases. ``` []((Q & <>R) -> ((!P & !R) U (R | ((P & !R) U (R | ((!P & !R) U (R | ((P & !R) U (R | (!P U R)))))))))) ```
- somethingsome 1y agoHey, if you have working (shearable) material that you use for teaching interns, I would be interested!
- AnimalMuppet 1y agoAs I understood that article, it seemed to be saying that formal methods often don't provide a good enough cost/benefit tradeoff to be worth it in many situations to many organizations. Right at the end, it basically says that your favorite underappreciated formal method isn't used because it costs too much and/or delivers too little. If an outfit that sells formal methods is saying that, then I suspect that (many) formal methods actually do cost too much for what benefit they deliver.
- rocqua 1y agoA key point they made is that formal methods, as currently practiced, have a cost-benefit curve that is very hockey-shaped. This doesn't really mean that the cost isn't worth it, but rather that it's hard to demonstrate the cost-effectiveness in a small pilot. It also means that the pay-off is fragile. Because apparently a lot of things need to come together for the value to show.
- pjmlp 1y agoUnless they are executable and part of the language tooling like SPARK, Dafny and co, I see little value coding an abstract model, that might be validated in theory, but hardly anyone will be able to cross-check if the manually written language ZYX code actually maps to the validated model. And then there are the code changes, which most likely devs aren't going back to the formal model to validate them, before applying the new set of changes.
- dataflow 1y agoI agree with you on the first paragraph, but the second one is something you could presumably enforce with tooling and during reviews, no?
- pjmlp 1y agoIn theory, in practice even enforcing unit tests is a challenge, and most code reviews end up being about code style than anything else, if they happen.
- bbkane 1y agoAWS recently mentioned something called PObserve in an ACM article. They said it checks logs emitted from the running application against the formal model. Sounds really useful for this exact problem; hopefully one day they'll open source it.
- pjmlp 1y agoI would need to check the article, although it sounds very fragile, expecting some logs are present in a specific format, and they actually tell the truth about what the code is doing.
- nickpsecurity 1y agoI believe you're way understating the difficulty of learning things like Alloy and doing theorem proving. Let's say I want to teach them non-formal, high assurance. That will involve safe subsets of their language, functional style of programming with inputs to outputs, isolation of side effects, and code reviews. They can do this without any extra or unusual knowledge. The basics of testing would likewise build on their existing knowledge. If their language supports it, static analyzers might work with the push of a button. Basic contracts might knock out many type or range errors without much thought. Basic tests go from their intuition to specific code implementing it. OK, now let's build models using relationships expressed in Alloy or TLA+. Now, they have to learn to think in a totally different way. They'll need new notations, new techniques. They'll have to put time into these not knowing the payoff. They'll also have far less or zero resources like StackOverflow or GeeksForGeeks that can solve the whole problem for them. Moving into theorem proverbs, they now have to know math or logic. They have to think formally. They have to specify the problem that way, keep it in sync with the English, do lots of work that might just be about limitations of the formal tool, and eventually they succeeded (or dont) at the proof. It's also a very, slow process vs informal methods of correctness checking. So, it's quite difficult to learn these things vs alternative methods. They also might have low or slow payoff while others payoff quickly and often. That's why I push using the alternatives first. Then, learning others overtime to gradually add them to your toolbox for when it makes sense: data structures, interface specification, highly-critical routines, etc.
- agentultra 1y agoIt’s not a free skill, for sure. There’s a spectrum of problems one can apply FMs to. Galois is probably selecting for the harder end of projects that do require PhDs with scary sounding degrees. In industry there are a lot of problems that don’t require that level of skill which can benefit a lot from application of FM’s.
- nickpsecurity 1y agoTo support your position, I still think the best ROI is interface specs with test generation and code level proofs. Also, detection of common problems like a type changing or no increment in a while. That would've caught many problems I've had in the last, few months. The biggest problem I see with that is how to specify those specs, especially contracts. I'd like to see a free collection of specs for common properties. Examples include ranges, ordering, not a value, invariants, and confidentiality. If searchable, then that might already be enough for many situations. From there, we can develop tools to generate them for people. The tools might parse the code, ask some questions, and generate the specs. Alternatively, LLM's trained on such things might generate specs. They might review them and suggest things. Over time, we'll also have more components that are already spec'd which specialists might build on. We just really need ways for developers to go from their situation to specs with no work or little work. If it's as easy as code and comments, we'll see more adoption.