[macintux]

Referenced at the very end; I came here to mention the sheer size of this effort. 60,000 lines is incredible. I can barely review 1,000 lines of Python without wanting to become a manual laborer instead.

> Ten years later their approach was fully machine-checked by the French computer scientist Georges Gonthier who verified 60,000 lines of formal language proof before declaring that their proof was indeed correct