7 ms·

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

> 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 ago
Formal 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 ago
 I 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 ago
 Ones 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 ago
 Go 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 ago
 Merge 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 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 c[k1] <= b[k2]) && (forall k1, k2 :: 0 <= k1 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?
 - ted_dunning 1y ago
 My intern this summer is teaching me about formal methods. You are hiring the wrong ones.
- almostgotcaught 1y ago
 > Formal methods can be understood by interns You're just repeating the same claim - yes I agree interns can also understand pytorch. Does that mean they can build prod LLM pipelines?
 - bravesoul2 1y ago
 Ah I think I see what you mean. For AI pipelines you need top guns anyway regardless of whether they use reversable or traditional computing.
 - almostgotcaught 1y ago
 > reversable or traditional computing o.O ... No man I'm saying a very simple and non-controversial thing: just because someone does a tut, has an elementary understanding, knows the basics, doesn't mean I'm going to let them build/maintain/own mission critical systems. It's not that deep.
 - bravesoul2 1y ago
 I see. But your point is then orthogonal. So it's $400/h not $100/h per SWE as you need experienced good people anyway. But the question really is: what solution minimises tbe number of those hours? Formal or informal?
 simiones 1y ago
 If I can build something in 100 hours paying 100$/hour, or 33 hours paying 400$/hour, I may well choose the 100 hours version. Which is why we hire interns in the first place, rather than only hiring senior architects for our companies.
 AnimalMuppet 1y ago
 Where do you work that you're paying interns 100$/hr and seniors 400$/hr, and are you hiring?
- anonzzzies 1y ago
 This might be your echo chamber of only working with phds? I have been doing fm for almost 40 years and, while it became easier, I can count people who actually understand what they are doing when programming on one hand, including seniors. Interns definitely don't understand and cannot learn to do formal methods generally. We see many companies inside as we do troubleshooting for large (fortune 500) companies to mid sized ones and these projects are short and urgent: we see a lot of code and, contrary to what you are saying or what seems to be the norm on HN, most people are really really bad at all they do; most we see cannot explain how the code actually works and indeed, often it's just beaten and trialed and errored until it has a facsimile of what it is supposed to do. There are no peer reviews often no version control and these systems run in massive hospitals, manage insurance, taxes or pensions for millions of people and so on. You are grossly overestimating the norm. If people did enjoy a uni degree, they generally look disgusted when you mention something like haskell as 'that useless stuff we had to to'. When I taught prolog in uni in NL, the students asked all the time why and why not c++ or java which would get them a job and make games. No one knows what formal methods even are.
 - simiones 1y ago
 While I agree with the gist of your argument, you should also note that "organizations that hire outside consultancies for urgent issues" is a self-selecting set of orgs with terrible coding practices. There are probably many more such orgs than GP would imagine, but they are not necessarily the norm, even though they are likely to represent the vast majority of what someone working for such a consultancy would see.
 - anonzzzies 1y ago
 I agree with that, however I think it is the majority. Being stuck in the largest companies in the world seeing the worst code makes me quite confident the majority sucks and the idea of that not being the case is just a huge outlier consumed by HN because of FAANG companies.
 - naasking 1y ago
 I'm not sure these people aren't capable of understanding, I think it's more a product of what you said: their projects were also short and urgent, and that sort of environment is not conducive to understanding, particularly given high churn where people are working on inherited code from people who also didn't have time to learn.

bravesoul2 1y ago

Formal 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 ago
I 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 ago
 Ones 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 ago
 Go 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 ago
 Merge 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 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 c[k1] <= b[k2]) && (forall k1, k2 :: 0 <= k1 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?
- ted_dunning 1y ago
 My intern this summer is teaching me about formal methods. You are hiring the wrong ones.
almostgotcaught 1y ago
> Formal methods can be understood by interns You're just repeating the same claim - yes I agree interns can also understand pytorch. Does that mean they can build prod LLM pipelines?
- bravesoul2 1y ago
  Ah I think I see what you mean. For AI pipelines you need top guns anyway regardless of whether they use reversable or traditional computing.
  - almostgotcaught 1y ago
    > reversable or traditional computing o.O ... No man I'm saying a very simple and non-controversial thing: just because someone does a tut, has an elementary understanding, knows the basics, doesn't mean I'm going to let them build/maintain/own mission critical systems. It's not that deep.
    - bravesoul2 1y ago
      I see. But your point is then orthogonal. So it's $400/h not $100/h per SWE as you need experienced good people anyway. But the question really is: what solution minimises tbe number of those hours? Formal or informal?
      - simiones 1y ago
        If I can build something in 100 hours paying 100$/hour, or 33 hours paying 400$/hour, I may well choose the 100 hours version. Which is why we hire interns in the first place, rather than only hiring senior architects for our companies.
        AnimalMuppet 1y ago
        Where do you work that you're paying interns 100$/hr and seniors 400$/hr, and are you hiring?
anonzzzies 1y ago
This might be your echo chamber of only working with phds? I have been doing fm for almost 40 years and, while it became easier, I can count people who actually understand what they are doing when programming on one hand, including seniors. Interns definitely don't understand and cannot learn to do formal methods generally. We see many companies inside as we do troubleshooting for large (fortune 500) companies to mid sized ones and these projects are short and urgent: we see a lot of code and, contrary to what you are saying or what seems to be the norm on HN, most people are really really bad at all they do; most we see cannot explain how the code actually works and indeed, often it's just beaten and trialed and errored until it has a facsimile of what it is supposed to do. There are no peer reviews often no version control and these systems run in massive hospitals, manage insurance, taxes or pensions for millions of people and so on. You are grossly overestimating the norm. If people did enjoy a uni degree, they generally look disgusted when you mention something like haskell as 'that useless stuff we had to to'. When I taught prolog in uni in NL, the students asked all the time why and why not c++ or java which would get them a job and make games. No one knows what formal methods even are.
- simiones 1y ago
  While I agree with the gist of your argument, you should also note that "organizations that hire outside consultancies for urgent issues" is a self-selecting set of orgs with terrible coding practices. There are probably many more such orgs than GP would imagine, but they are not necessarily the norm, even though they are likely to represent the vast majority of what someone working for such a consultancy would see.
  - anonzzzies 1y ago
    I agree with that, however I think it is the majority. Being stuck in the largest companies in the world seeing the worst code makes me quite confident the majority sucks and the idea of that not being the case is just a huge outlier consumed by HN because of FAANG companies.
- naasking 1y ago
  I'm not sure these people aren't capable of understanding, I think it's more a product of what you said: their projects were also short and urgent, and that sort of environment is not conducive to understanding, particularly given high churn where people are working on inherited code from people who also didn't have time to learn.