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?

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

For someone who has never done React or Formal? Probably about the same learning curve.

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.