When I was at grad school most of my research was about devising highly impractical (but kinda cute) algorithms for idealized machines with concurrent processes. These algorithms were usually about twenty lines long, but the correctness proof would span a dozen pages (and sometimes several hundred numbered equations) - at one point a reviewer got so disgusted that they called it "Proof by intimidation".
So, yeah, imagine doing that for any program with more than five hundred lines of code.
So, yeah, imagine doing that for any program with more than five hundred lines of code.