To be a better programmer, write little proofs in your head
the-nerve-blog.ghost.io
To be a better programmer, write little proofs in your head
1–10 of 181 posts
Re: To be a better programmer, write little proofs in your head
#2Oh, 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 Programming Pearls, gave the task of writing an ordinary binary search to a group of professional programmers at IBM, and found that 90% of their implementations contained bugs. The most common one seems to have been accidentally running into an infinite loop. To be fair, this was back in the day when integer overflows had to be explicitly guarded against - but even then, it's a surprising number.
[1]: https://hiandrewquinn.github.io/til-site/posts/binary-search...
Re: To be a better programmer, write little proofs in your head
#3Now if we can get LLMs to do that, they might code better. Proofs are a lot of work, but might keep LLMs on track.
Re: To be a better programmer, write little proofs in your head
#4Writing correct proofs is hard. Program verification is hard. In my opinion if you are hand weaving it there’s no benefit. Thinking about invariants and pre-post conditions is often unnecessary or greatly reduced if you write idiomatic code for the language and codebase. Check out “The Practice of Programming” by R. Pike and B. W. Kernighan. The motto is: simplicity, clarity, generality. I find it works really well in a day job.
On a slightly related note… Competitive programming is surprisingly good at teaching you the right set of techniques to make sure your code is correct. You won’t progress beyond certain stage unless you pick them up.
Re: To be a better programmer, write little proofs in your head
#5> 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 of the data layout and code dependencies. 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.
Re: To be a better programmer, write little proofs in your head
#6Writing correct proofs is hard. Program verification is hard. In my opinion if you are hand weaving it there’s no benefit. Thinking about invariants and pre-post conditions is often unnecessary or greatly reduced if you write idiomatic code for the language and codebase. Check out “The Practice of Programming” by R. Pike and B. W. Kernighan. The motto is: simplicity, clarity, generality. I find it works really well i…
Turn your first paragraph on its head:
Appropriate abstractions (i.e., "idiomatic code for the language and codebase") make program verification easy. If you are hand-weaving an appropriately-abstracted program, there's little benefit to thinking about loop invariants and pre-post conditions, since they don't exist at that level of generality: correct proofs follow directly from correct code.
Re: To be a better programmer, write little proofs in your head
#7I learned the foundations of theoretical computer science in university. I agree with the sentiment of this post, though it is hard to perform in practice.
In addition to pre-conditions and post-conditions, I would like to emphasize that loop invariants and structural induction are powerful techniques in CS proofs. https://en.wikipedia.org/wiki/Loop_invariant , https://en.wikipedia.org/wiki/Structural_induction
These notes from UofT's CSC236H are on-topic: https://www.cs.toronto.edu/~david/course-notes/csc236.pdf#pa...
Re: To be a better programmer, write little proofs in your head
#8Writing correct proofs is hard. Program verification is hard. In my opinion if you are hand weaving it there’s no benefit. Thinking about invariants and pre-post conditions is often unnecessary or greatly reduced if you write idiomatic code for the language and codebase. Check out “The Practice of Programming” by R. Pike and B. W. Kernighan. The motto is: simplicity, clarity, generality. I find it works really well i…
Have to strongly disagree here. I don't think the OP meant thinking up a complete, formal, proof. But trying to understand what kind of logical properties your code fulfills - e.g. what kind of invariants should hold - will make it a lot easier to understand what your code is doing and will remove a lot of the scare factor.
Re: To be a better programmer, write little proofs in your head
#9The software he’s working on seems rather obscure and perhaps not launched yet? get-nerve.com can’t be resolved.
Re: To be a better programmer, write little proofs in your head
#10What's interesting about this view is that theorem provers ultimately boil down to sufficiently advanced type checking (the book Type Theory and Formal Proof is an excellent overview of this topic). Literally the heart of proof assistants like Lean is "if it compiles, you've proved it".
So more practical type systems can be viewed as "little" theorem provers in the sense the author is describing. "Thinking in types" so to speak, is mathematically equivalent to "writing little proofs in your head". I would also add that merely using types is not equivalent to "thinking in types" as one would be required to do writing a sufficiently advanced Haskell program.