Program correctness

This week, the focus of you lectures have moved towards program correctness, which is more or less a formalization of proving that your code does what it should. I found this topic to actually be quite intuitive and something I had been doing in a much less rigorous and formal way in my head when planning my code. I also know have more of an appreciation for the somewhat draconionan rules we had for program style, most of which was directed towards making your code both readable and breaking it up into smaller parts. The idea of smaller blocks of code with helper function especially seems useful now since trying assess the correctness of a large block of text is far more daunting then the same code broken up into several parts. However, applying the proof methods we've learned to program correctness feels infinitely more tedious, with the attention to detail required being astronomically greater. I can't imagine how development teams would manage to be able to prove their code correct for a major project like an operating system. Unfortunately suspect that they don't, though I also suspect our computers would benefit greatly if the did.