In this context it's proofs of properties about the program you're writing. A classic one is that any lossless compression algorithm should satisfy decompress(c

In this context it's proofs of properties about the program you're writing. A classic one is that any lossless compression algorithm should satisfy decompress(compress(x)) == x for any x.