3 ms·

> 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

• 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 < 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?
    • bubblyworld 1y ago
      Hah, nice one! I didn't know about multiset when I went about this (some years ago) and ended up proving all sorts of facts about sorted sets and partitions. I think you've changed my mind, actually, thank you. I still maintain that this requires more mathematical maturity than diving into react, but I may be saying that out of ignorance of react's internals =P
  • bravesoul2 1y ago
    For someone who has never done React or Formal? Probably about the same learning curve.
    • bubblyworld 1y ago
      I suspect we are falling into the classic human trap of measuring a complex topic using a linear scale. But the sibling comment convinced me formal methods are more approachable than I thought, for sure.