And codes does what code does. Given some binary executable, an alien reading it far in the future should be able to understand what's going on, at least if th

And codes does what code does. Given some binary executable, an alien reading it far in the future should be able to understand what's going on, at least if they understand the architecture. :P I've written a few machine checked proofs, and there's really two ways that I've seen, either writing it for the next human to read, or just enough that the checker accepts it. The latter makes free use of tactics like `crush`, which brute force solutions out of current assumptions, exploring the search space automatically. That's really convenient, but can make reading the proof very un-enlightening.