Turner hoped that we could have programming languages that wouldn't go into (useless) infinite loops. They should either terminate, or keep producing values forever (be 'productive').

The author sets out to prove that Bird's version of the prime number generator (Sieve of Eratosthenes) is productive.

Fwiw I'm lost almost immediately in section 4 - the actual proof.

I think I get one point, which is to immediately ignore the actual values of the primes, and only prove that they keep being generated (which I guess is the purpose of `approx`), but I'm immediately lost by the overall strategy:

  that is, not so much showing that primes spec is a fixed point of makeP · makeC, but that it is the least fixed point.