really appreciate this post.
1) i did a quick skim of the predicate transformer wp page, looking at weakest preconditions and taking a short detour onto the definiton of hoare triples. i _think_ it is about minimal pre-statement (statement being the active code in question) assertions and maximal post-statement assertions and using that as a basis to define your program/algorithms. this leads to strong conclusions about the correctness of your code. i would say this is a great and perhaps necessary goal for important systems. i try to do it at a slightly higher and less rigorous level with automated tests, but the desire is the same, and if i really wanted correct code, i would probably do just this sort of thing.
2) i've been programming for a while. about a year and a half ago i noticed that i was falling into this bad habit that i had worked hard to get out of many years ago where i would just take a stab in the dark, tweak some code, and run my program over and over until the output was correct. :feelsbadman: since that time, i have made an effort to develop a habit of thinking much more before running my code, and it is showing results. often i can write code for hours, once recently i even did so for days, and not execute it, reasoning as much as possible about execution and state along the way, and when i finally run it, there are bugs but they are usually quite shallow and i can fix them quickly and then bam! it just works. sometimes i pause in this and for the satisfaction of running my new code i will write automated tests that check the correctness of some of the functionality. and i have paused at times and written in my notebook, explaining to myself what the problem is that i am trying to solve, why my current solutions have failed, and reasoning about what a good and working solution might look like, and designing it before opening the IDE. that works wonders too. i would say again - i'm not quite as rigorous as he was, but the method has helped me write better code.
3) yes, i have done this before, and i try to emulate the idea in my (high level) code. but i'm definitely not at that rigorous level :)
and thank you for the reminder to avoid wasting time.
Neil Gaiman has a speech called "Make Good Art" and i read the transcript (he has made a short book out of it) and watched a video of him actually delivering the speech at a graduation ceremony yesterday. i will conclude with a quote from that speech.
> There was a day when I looked up and realized that I had become someone who professionally replied to email, and who wrote as a hobby. I started answering fewer emails, and was relieved to find I was writing much more.