The rabbit hole goes deeper: how are you sure the compiler is correct? See the paper by John Regehr and his group: http://blog.regehr.org/archives/492
I'm not just saying this randomly in any subject that is concerned with correctness, as Regehr's work clearly shows that the places where compilers make the most mistakes are the places that cryptographic functions play in: numeric calculations at the boundaries of what is representable.
I also want to point out that Lipton's first suggestion is to basically have very smart unit tests - which is a good suggestion. If your result should have known properties, test those.
I'm not just saying this randomly in any subject that is concerned with correctness, as Regehr's work clearly shows that the places where compilers make the most mistakes are the places that cryptographic functions play in: numeric calculations at the boundaries of what is representable.
I also want to point out that Lipton's first suggestion is to basically have very smart unit tests - which is a good suggestion. If your result should have known properties, test those.