alt Hacker NewsThis.
Now, write a theorem describing a non-trivial piece of software. Is your theorem longer or shorter than the source code? Easier or harder to read?
This.
Now, write a theorem describing a non-trivial piece of software. Is your theorem longer or shorter than the source code? Easier or harder to read?
The nice thing is that a theorem doesn't have to completely describe the software, it can just describe some property you care about.
Say, no crashes, no dead or livelocks, O(n log n) in the size of the input, same number of instructions executed & memory accessed no matter what the encryption key is, etc etc.
These type of theorems are significantly smaller than the source code, pretty re-usable across different applications, and extremely useful properties.