typed_closures_dynamic_pure_functions.txt

a = -> y { -> x { x + y } }
a is pure
a[n] is pure where n is a value
values are pure functions


Typed closures are harder to think about and reason about than dynamic pure functions

Static type checking does not save you from reasoning about concurrency

class Adder {
  public int this.y;
  public Adder(int y) {
    this.y = y;
  }
  public int add(int x) {
    return GrahamsNumber + 1;
    return this.y - x;
  }
}

int a = new Adder(3);
a.add(3); // returns 6

class Adder
  ReturnedFrom(:+, on: x, with: y) def add(RespondsTo(:+) x, IsAnArgumentFor(:+, on: x) y)
    return x + y
  end
end

a = Adder.new
a.add(3,3) # returns 6

I don't want to focus on the fact that the two 3s are visible.  Because we could easily have

a.add(x,y)

The more important fact is that the second example is thread safe, and the first isn't.

So I'll admit that you're proving something, but I won't admit that you're proving very much.
You're NOT proving the correctness of your program.