Thanks to influence from Dijkstra, Wirth, et al in my formative years, when I program I construct a (usually informal) correctness proof simultaneously (well, k

Thanks to influence from Dijkstra, Wirth, et al in my formative years, when I program I construct a (usually informal) correctness proof simultaneously (well, kind of interleaved) with my construction of the code. The two constructions assist one another and converge to procedures which solve the required problem. I find this approach more productive than an ad hoc (hack & debug until done) approach. The correctness proof supports the correctness of the solution and the solution is usually more elegant (simpler, etc.). I annotate the code with elements of the proof to assist with maintenance. I think that most programmers do this to some degree, i.e. have an internal argument about why what they're doing will work and include some assertions and comments, etc. When I'm given some hunk of complex procedural code lacking strong types, preconditions, postconditions, invariants, arguments bridging such, etc. I don't find it very useful. Proving the correctness of complex ad hoc code is often harder than just solving the problem again from scratch. There are AI automated reasoning systems (based on incremental theorem provers) that can help me write good code and I follow the evolution of such tools. So far, the code I'm seeing from llm systems seems like a maintenance and reliability nightmare.