This is something I’ve practiced myself quite a lot in recent years, and in my experience it’s so much harder while at your desk. Doing something else while letting your brain work really helps. For me, that’s usually going for a walk, taking a run in the woods, or doing some repeditive household chore.
To be a better programmer, write little proofs in your head
61–70 of 181 posts
Re: To be a better programmer, write little proofs in your head
#62> My thesis so far is something like "you should try to write little proofs in your head about your code." But there's actually a secret dual version of this post, which says "you should try to write your code in a form that's easy to write little proofs about." Easier said than done. It is certainly feasible on greenfield projects where all the code is written by you (recently), and you have a complete mental model…
> when they modify global state and are written by different developers.
Once cancer has metastasized, the treatment plans are more aggressive and less pleasant. The patient can still be saved in many cases, but that depends on a lot of external factors.
Re: To be a better programmer, write little proofs in your head
#63I think I stumbled across a similar concept in the more difficult post-grad classes I ended up in a long time ago. I began at some point late in my undergrad doing math tests entirely in pen. I didn't understand why, but it resulted in higher scores almost always, and much neater scratchwork, which I had attributed to the reason, but I think what was helping was something along the lines of what this post is getting at.
What was helping me was that before I wrote a single expression, I thought about it carefully in my head and where it would lead before putting pen to paper, because I didn't want to make a bunch of messy scratch out marks on it. Or, sometimes, I'd use a healthy amount of throwaway scratch paper if allowed. Once my path was fully formed in my head I'd begin writing, and it resulted in far fewer mistakes.
I don't always take this approach to writing code but often I do formulate a pretty clear picture in my head of how it is going to look and how I know it will work before I start.
Re: To be a better programmer, write little proofs in your head
#64> My thesis so far is something like "you should try to write little proofs in your head about your code." But there's actually a secret dual version of this post, which says "you should try to write your code in a form that's easy to write little proofs about." Easier said than done. It is certainly feasible on greenfield projects where all the code is written by you (recently), and you have a complete mental model…
> It's much harder to prove stuff this way when you call foo(), bar() and baz() across unit boundaries, when they modify global state and are written by different developers. I think this reinforces the article's point. Code like this is much more likely to contain bugs and be harder to maintain without introducing more bugs, than programs written from the outset with this goal of "provability".
I just finished cave diving in a code base that's had a very old ticket to clean up the mess.
I went in with 3 tickets in mind to fix. I found half a dozen more while I was down there, and created 2 myself. I don't know if I got off easy or I was distracted and missed things.
The other project I'm working on is not dissimilar. Hey did you guys know you have a massive memory leak?
Re: To be a better programmer, write little proofs in your head
#65While having been employed as a developer for almost 7 years now, I remember taking this class maybe discrete math, I was not a fan of that class, where you have problems like p -> q
Also farthest in math/physics I got was intro to quantum mechanics which the multiple-pages to solve a problem lost me
Being a good programmer... I don't have a degree so I've never really tried to get into FAANG. I also am aware after trying Leetcode, I'm not an algorithm person.
What's funny is at my current job which it's a multi-national huge entity thing but I have to try and push people to do code reviews or fix small errors that make something look bad (like a button being shorter than an input next to it).
I am self-aware with true skill, I can make things, but I don't think I'd ever be a John Carmack. If you follow a framework's pattern are you a good developer? I can see tangible metrics like performance/some slow thing, someone better makes it faster.
Recently someone forked a repo of a hardware project I made. It's fun watching them change it, to understand what I wrote and then change it to fit their needs.
When I see my old code I do recognize how it was verbose/could be much simpler.
Re: To be a better programmer, write little proofs in your head
#66The best way I have found to integrate this approach is Test Driven Development.
When done well, every test you write before you see it fail and then you write the barest amount of code that you think will make it pass is a mini-proof. Your test setup and assertions are what cover your pre/post conditions. Base cases are the invariant.
The key here is to be disciplined, write the simplest test you can, see the test fail before writing code, write the smallest amount of code possible to make the test pass. Repeat.
The next level is how cohesive or tightly coupled your tests are. Being able to make changes with minimal test breakage "blast radius" increases my confidence of a design.
Re: To be a better programmer, write little proofs in your head
#67Why not include little proofs in the code when you can? Several programming languages and libraries support Design-by-Contract ( https://en.wikipedia.org/wiki/Design_by_contract ) which lets you specify preconditions, postconditions, and invariants directly in your code. Those predicates can be checked in various ways (depending on how deeply Design-by-Contract is supported) to help you know that your code is working…
Even standard assertions work as a version of this
Standard assertions certainly are better than keeping the little proofs only in your head.
Many Design-by-Contract implementations are nicer than standard assertions because they help to express intent better and easily refer to the 'old' value of a parameter to verify desired results.
Re: To be a better programmer, write little proofs in your head
#68The best way I have found to integrate this approach is Test Driven Development. When done well, every test you write before you see it fail and then you write the barest amount of code that you think will make it pass is a mini-proof. Your test setup and assertions are what cover your pre/post conditions. Base cases are the invariant. The key here is to be disciplined, write the simplest test you can, see the test f…
[deleted]
Re: To be a better programmer, write little proofs in your head
#69Earlier quoted context omitted.
That's a really funny example, given how many bugs have been found in C programs because idiomatic loops are wrong in the edge cases. How do you idiomatically write a loop to iterate over signed ints from i to j (inclusive) in increasing order, given i What does that loop do when j is INT_MAX?
I can imagine someone who sketches out little proofs in their head - or even on paper - missing that case too. It’s easy to forget you’re not doing normal arithmetic when doing arithmetic in C!
Yeah, it's a hard case in general. But C's idioms really don't encourage you to think about it. You really need to default to a loop structure that checks the termination condition after the loop body but before the increment operation for inclusive end coordinates.
It's easy to think that's what do/while is for, but it turns out to be really hard to do the increment operation after the conditional, in general. What you really want is a loop structure with the conditional in the middle, and the only general purpose tool you get for that is a break. C (or any language with similar syntax) really doesn't have an idiom for doing this correctly.
Re: To be a better programmer, write little proofs in your head
#70Oh, I have a relevant and surprisingly simple example: Binary search. Binary search and its variants leftmost and rightmost binary search are surprisingly hard to code correctly if you don't think about the problem in terms of loop invariants. I outlined the loop invariant approach in [1] with some example Python code that was about as clear and close to plain English at I could get. Jon Bentley, the writer of Progra…
What are the odds you write a binary search that you'll use more than once instead of just running it and writing down the result?