Formal CSS

Or "How to write a program without trying"

The formal css proof is here. It's a gzip'd tar file of Lego source code.

This is a mathematical proof that an abstract mathematical relation known as CSS has an output for every input.

This is entirely abstract mathematics — no mention of computers, programs, or computability, in sight.

But inevitably — due to the Curry-Howard isomorphism — our proof contains a program implementing CSS.

The theorem prover I used to write the proof - Lego - can directly interpret the proof as a program, although very inefficiently.

Possession of such a program is illegal in the US & maybe elsewhere? Does that make this proof illegal too?

:-)