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

1 hour 45 min ago

3 hours 9 min ago

4 hours 36 min ago

5 hours 46 min ago

6 hours 27 min ago

9 hours 15 min ago

10 hours 19 min ago

12 hours 39 min ago

18 hours 11 min ago

19 hours 24 min ago