4 ms·
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 de
by avg_dev 3y ago
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.
- rramadass 3y agoI am glad you found it useful; your appreciation is much appreciated :-) The point of my post was that studying Dijkstra is essential even if we cannot follow his methods to the letter. The key is to improve our own thinking and adopt better and more productive work-habits. You might also want to checkout Dijkstra's A Method of Programming and Wirth's Systematic Programming: An Introduction.