# 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?