Concerning Correctness

Well, we've been handling correctness lately. It's always been kind of neat to me, representing sort of a meshing and intersection of the worlds of purely theoretical and logical thought with normal code. At first, I still couldn't really appreciate the necessity of proving the correctness of code, but over the last little while I've come to realize that it generally makes the bizarre cases something should be handling a lot more apparent just by writing it out in the context of a proof, as opposed to some IDE. In any case, I've found it generally not too rough, though I have had a bit of trouble rationalizing the need for loop invariants to myself, when it seems they're usually something like n is always a natural number, which *seems* self-evident, but I imagine it's necessary when trying to prove more complicated code.