Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

To be a better programmer, write little proofs in your head

the-nerve-blog.ghost.io

Post reply on HN
Print view View original

161–170 of 181 posts

Re: To be a better programmer, write little proofs in your head

#161

Post by hiAndrewQuinn »

Etheryte wrote: post #153
mdnahas wrote: post #144

Earlier quoted context omitted.

I read about this and started using binary search as my interview question. It worked well - about 2/3rds of highly credentialed applicants could not write a working implementation in 20 minutes. Most failures went into an infinite loop on simple cases! The ones who could write it usually did so quickly. I think part of reason is that most people were taught a bad interface. Even the code on Wikipedia says “Set L to…

Based on your description, it sounds like a bad interview question. When otherwise capable candidates can't answer your trivia, maybe it isn't a useful signal? More than anything, it just sounds like you're selecting for people who practiced leetcode vs those who didn't.

To be precise, Zoz said

>about 2/3rds of highly credentialed applicants

Credentialed ≠ capable.

Re: To be a better programmer, write little proofs in your head

#162

Post by hoseja »

monkeyelite wrote: post #78
hiAndrewQuinn wrote: post #2

Oh, 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…

The C++ standard library phrases binary search as a partitioning problem - finding the index where a predicate goes from false to true, which is helpful for me.

Recalling the subtle difference between std::lower_bound and std::upper_bound and where it matters is somewhat annoying before it becomes muscle memory.

Re: To be a better programmer, write little proofs in your head

#163

Post by irchans »

This might be the best article that I have read this year. It might change the way that I program. I really want to write up examples for each of the ideas presented: Monotonicity, Pre- and post-conditions, Invariants, Isolation, Induction, and Proof-affinity as a quality metric. I think it's easy to find these ideas in my code, but I want to try to practice writing proofs "in my head" as I code to make my code better. It is not apparent to me now how this will work, but if I write up some examples, I imagine it will become clearer.

Re: To be a better programmer, write little proofs in your head

#164

Post by Izkata »

wizzwizz4 wrote: post #104
chowells wrote: post #69

Earlier quoted context omitted.

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…

This may be hubris, but… int i = start; do thing_with(i) while (i++

Isn't i going to be one past end on the last iteration?

I think you want either "++i (Using "<=" in a termination condition has become a code smell for me, it's been wrong more often than not, so it sticks out as "pay close attention here")

Re: To be a better programmer, write little proofs in your head

#165

Post by rockostrich »

hiAndrewQuinn wrote: post #160
mdnahas wrote: post #144

Earlier quoted context omitted.

I read about this and started using binary search as my interview question. It worked well - about 2/3rds of highly credentialed applicants could not write a working implementation in 20 minutes. Most failures went into an infinite loop on simple cases! The ones who could write it usually did so quickly. I think part of reason is that most people were taught a bad interface. Even the code on Wikipedia says “Set L to…

Indeed, this is actually one reason why I like Python's closed-left, open-right syntax. It lets us sidestep the inclusive bound issue entirely, because, as noted in the post, for all 0 ≤ l ≤ r ≤ len(L) where L is a Python list, L == L[0:len(L)] == L[0:l] + L[l:len(L)] == L[0:l] + L[l:r] + L[r:len(L)] I actually didn't like this syntax until I had to work this out. Now everyone else's approach seems silly to me.

Don't most slice methods behave this way? Javascript's `Array.prototype.slice`, Java's `Arrays.copyOfRange`, Golang's slicing syntax is similar to Python's except the 3rd value is the max size of the resulting slice rather than the step value all behave this way.

Re: To be a better programmer, write little proofs in your head

#166

Post by chowells »

Izkata wrote: post #164
wizzwizz4 wrote: post #104

Earlier quoted context omitted.

This may be hubris, but… int i = start; do thing_with(i) while (i++

Isn't i going to be one past end on the last iteration? I think you want either "++i (Using "<=" in a termination condition has become a code smell for me, it's been wrong more often than not, so it sticks out as "pay close attention here")

Actually, I think what you really need is "i++ != end". The whole point was inequalities don't work how you want when end is INT_MAX. You want to just terminate after the loop body where i was equal to end. Except now I'm not sure if that evades the UB of a signed int exceeding INT_MAX. I don't know C well enough to know if the UB is in performing the increment or reading the value afterwards.

Edit: Just checked in with a C expert. The UB is in the increment operation, so that's not correct after all. You really do just need to separate out the update from the test entirely.

Re: To be a better programmer, write little proofs in your head

#167

Post by NewCalculadora »

Totally agree — binary search is the classic example of something that feels simple until you try to implement it robustly. The off-by-one errors, incorrect mid-point updates, and forgetting to handle edge cases (like low == high) are so easy to miss.

Bentley’s anecdote is a perfect illustration of how writing "correct" code often depends more on reasoning rigor than language syntax. Loop invariants, like you mentioned, are key here — they help anchor the logic through each iteration. It’s one of those patterns that separates surface-level understanding from deep intuition.

I also like how languages like Rust (with its strong type system) or Python (with clarity) can highlight these logic gaps early, especially in interviews or algorithmic codebases.

If you’ve got the link to your example post handy, I’d love to give it a read.

Re: To be a better programmer, write little proofs in your head

#168

Post by aljgz »

pclowes wrote: post #100
aljgz wrote: post #86

Earlier quoted context omitted.

Consider a function that gets an array of integers and a positive number, and returns the sum of the array elements modulo the number. How can we prove using tests, that this always works for all possible values? Not discounting the value of tests: we throw a bunch of general and corner cases at the function, and they will ring the alarm if in the future any change to the function breaks any of those. But they don't…

I would lean towards types and property testing here using tools like Coq.

Can you elaborate?

Re: To be a better programmer, write little proofs in your head

#169

Post by trealira »

chowells wrote: post #166
Izkata wrote: post #164

Earlier quoted context omitted.

Isn't i going to be one past end on the last iteration? I think you want either "++i (Using "<=" in a termination condition has become a code smell for me, it's been wrong more often than not, so it sticks out as "pay close attention here")

Actually, I think what you really need is "i++ != end". The whole point was inequalities don't work how you want when end is INT_MAX. You want to just terminate after the loop body where i was equal to end. Except now I'm not sure if that evades the UB of a signed int exceeding INT_MAX. I don't know C well enough to know if the UB is in performing the increment or reading the value afterwards. Edit: Just checked in w…

Yeah, it would have to be something like this if you wanted to avoid the signed integer overflow at the end of the loop:

  assert(i
Post reply on HN