I literally don't even write proofs in my head. Every time I write algo I just ask Cursor for a Lean/Rocq proof of correctness. No tests. No test coverage. The sheer power of type theory
To be a better programmer, write little proofs in your head
171–180 of 181 posts
Re: To be a better programmer, write little proofs in your head
#172Earlier quoted context omitted.
I knew about the infamous Binary Search bugs in books, and I dared to write the first bug-free implementation in my book, very carefully. Still, it ended up having bugs. :) Luckily, Manning's early access program let me fix them before printing.
Oh interesting, where can we read about the bug that was there?
It was quite silly. The most common bug with binary search is calculating the middle point: `(start + end) / 2`. It looks straightforward, but "start + end" could cause an integer overflow for large data structures, and that would break the function. IIRC, my handling for that case also turned out to be incorrect, and one of the readers caught it. I don't remember if there were other bugs, there could be, but that one hurt the most :)
Re: To be a better programmer, write little proofs in your head
#173Earlier quoted context omitted.
Oh interesting, where can we read about the bug that was there?
It was quite silly. The most common bug with binary search is calculating the middle point: `(start + end) / 2`. It looks straightforward, but "start + end" could cause an integer overflow for large data structures, and that would break the function. IIRC, my handling for that case also turned out to be incorrect, and one of the readers caught it. I don't remember if there were other bugs, there could be, but that on…
Ah yes this is the "classic" bug that was in the Java standard library undiscovered for twenty years, iirc.
I find this topic really interesting, thanks for sharing. I doubt I could code a binary search without any bugs from scratch :)
Re: To be a better programmer, write little proofs in your head
#174Earlier quoted context omitted.
> Tests do not ensure that your functions are correct; they ensure that you are alerted when their behavior changes. I agree with that part and I am not against tests, just the idea of writing tests first. > helps you design good interfaces I am sure plenty of people will disagree but I think testability is overrated and leads to code that is too abstract and complicated. Writing tests first will help you write code…
>It makes sense at a high level though This is the way I've always done TDD. I don't think it makes sense to do it any other way. If a test case doesn't map on to a real scenario you're trying to implement the code for it doesn't make any sense to write it. I find that people who write the test after tend to miss edge cases or (when they're trying to be thorough) write too many scenarios - covering the same code more…
> I don't think I've written any production code in years where I gave up because it was intrinsically not possible.
What I meant by "not possible" is writing both sides of the API at the same time. For example, you write a library for overlaying maps on video feeds, it is good if you are also writing the application that uses it. For example a drone controller. So in the early phase, you write the library specifically for your drone controller, changing the API as needed.
But sometimes, the drone controller will be made by another company, or it may be a project too big not to split up, that's the "not possible" part. And without a clear, in control use case, you have to make guesses, and writing tests can help make good guesses.
Re: To be a better programmer, write little proofs in your head
#175Earlier quoted context omitted.
This makes for an interesting test. I checked Claude Sonnet, just for the he'll of it Prompt: Please write a bug free binary search in python Answer: def binary_search(arr, target): """ Performs binary search on a sorted array. Args: arr: A sorted list of comparable elements target: The element to search for Returns: The index of target if found, -1 otherwise """ left = 0 right = len(arr) - 1 while left # Example usa…
Very good! Looks good to me. One small callout: mid = left + (right - left) // 2 This implementation detail is to my knowledge unnecessary in Python because Python's built-in int type has arbitrary-precision integers. It's intended to avoid buffer overflows in languages like C. Imagine, say, that left is 1 and right is 2^63 - 1. In Python left + right will just give you 2^63, no big deal. In C, left + right will over…
IIRC you're correct, but the comment is a red herring.
In Python, the double slash (or type casting) is necessary as a single slash will yield a float by default. Double slash returns an int.
Re: To be a better programmer, write little proofs in your head
#176Even better: Use comments to "prove" your code:
// x == 0 && (y == 0 || y == x + 1) && a[x + y] != 0
... code here ...
// x == 0 && (y == x + 1) && ...
Re: To be a better programmer, write little proofs in your head
#177Earlier quoted context omitted.
>It makes sense at a high level though This is the way I've always done TDD. I don't think it makes sense to do it any other way. If a test case doesn't map on to a real scenario you're trying to implement the code for it doesn't make any sense to write it. I find that people who write the test after tend to miss edge cases or (when they're trying to be thorough) write too many scenarios - covering the same code more…
> I don't think I've written any production code in years where I gave up because it was intrinsically not possible. What I meant by "not possible" is writing both sides of the API at the same time. For example, you write a library for overlaying maps on video feeds, it is good if you are also writing the application that uses it. For example a drone controller. So in the early phase, you write the library specifical…
>What I meant by "not possible" is writing both sides of the API at the same time. For example, you write a library for overlaying maps on video feeds
If I were doing this I would probably start by writing a test that takes an example video and example map and a snippet of code that overlays one on to the other and then checks the video at the end against a snapshot.
>But sometimes, the drone controller will be made by another company, or it may be a project too big not to split up, that's the "not possible" part. And without a clear, in control use case, you have to make guesses, and writing tests can help make good guesses.
This is the figuring out the requirements part. If you are writing an API for another piece of software to call you might have to do some investigation to see what kind of API endpoint it expects to call.
Re: To be a better programmer, write little proofs in your head
#178I 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…
When I was in eighth grade my advanced algebra teacher said "I wonder if you always did your homework in pen, would you make fewer mistakes." That was 45 years ago. Now I am a mathematician and I have done 95% of my math in pen since then. I'm not sure how much it helped, but as you said maybe I think a bit more before I write because I don't like scratching out mistakes.
Re: To be a better programmer, write little proofs in your head
#179correlated ideas, that I thought were worth sharing:
- formal properties help one understand their own code better. This holds even more true when the properties are high level.
- they are useful to make sure the code behaves as expected, but not only. During the development, it notably helps finding better implementations and reviewing incremental changes.
- the process of outlining properties and drafting their proofs is already valuable, even without formally doing the proofs. It often prompts ideas about more properties and potential bugs.
- a great code is one that makes its rules and invariants obvious. This usually correlates well with general readability.
Re: To be a better programmer, write little proofs in your head
#180Totally tangential, but I love to read post-mortems of people fixing bugs. What were the initial symptoms? What was your first theory? How did you test it? What was the resolution? Raymond Chen does this a lot and I've always enjoyed it. I learn more from these concrete case studies than from general principles (though I agree those are important too). One of my most recent bugs was a crash bug in a thread-pool that…
> Totally tangential, but I love to read post-mortems of people fixing bugs. I know I already posted it moons ago but... Around 1991 I made a little game, similar to Canon Ball on the MSX (which later on Pang / Buster Bros did copy). I had one weird case where sometimes the game would crash. Plain crash. But sometimes after playing for 15 minutes and already passing several levels. I just couldn't find it. I couldn't…
Wow! Saving all input sounds extreme to solve a bug, but I agree it paid dividends in the long run.
Nice story.