In case this one went under the radar, at POPL'12, Martín Escardó gave a tutorial on seemingly impossible functional programs:

Programming language semantics is typically applied to

prove compiler correctness and allow (manual or automatic) program

verification. Certain kinds of semantics can also be applied to

discover programs that one wouldn't have otherwise thought of. This is

the case, in particular, for semantics that incorporate topological

ingredients (limits, continuity, openness, compactness). For example,

it turns out that some function types (X -> Y) with X infinite (but

compact) do have decidable equality, contradicting perhaps popular

belief, but certainly not (higher-type) computability theory. More

generally, one can often check infinitely many cases in finite time.

I will show you such programs, run them fast in surprising instances,

and introduce the theory behind their derivation and working. In

particular, I will study a single (very high type) program that (i)

optimally plays sequential games of unbounded length, (ii) implements

the Tychonoff Theorem from topology (and builds finite-time search

functions for infinite sets), (iii) realizes the double-negation shift

from proof theory (and allows us to extract programs from classical

proofs that use the axiom of countable choice). There will be several

examples in the languages Haskell and Agda.

A shorter version (coded in Haskell) appears in Andrej Bauer's blog.

## Recent comments

2 weeks 2 days ago

2 weeks 3 days ago

2 weeks 3 days ago

2 weeks 5 days ago

2 weeks 5 days ago

2 weeks 5 days ago

2 weeks 5 days ago

2 weeks 6 days ago

2 weeks 6 days ago

4 weeks 13 hours ago