I would strongly recommend to read the released books TAOCP of D.E.Knuth (The Art of Computer Programming) and other works of him and his students. He describes and has always cared about the ability to prove a computer algorithm mathematically. I think besides his own MMIX language, C is an excellent language to write algortithms that hold mathematical validations, since C is well defined and so are most parts of libc. I think this is the only approach to algorithms that are really invariant. There is now "external" tool to test "internal" invariance of algorithms since this would mean to test an algorithm with all conditions that could ever appear. The checksum approach isn't quite usefull I think, since algorithms are and should be changed by hand and communication between developers should be done as direct as possible. If you introduce checksums, you provide a tools that simulates stability where there is none. There is no fire and forget algorithm that you haven't develeoped and documented quite well.
