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

31–40 of 181 posts

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

#31

Post by GMoromisato »

Totally 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 used garbage-collected objects (this is in C++) to manage network connections. Sometimes, during marking, one of the objects I was trying to mark would be already freed, and we crashed.

My first thought was that this was a concurrency problem. We're supposed to stop all threads (stop the world) during marking, but what if a thread was not stopped? Or what if we got an event on an IO completion port somehow during marking?

I was sure that it had to be a concurrency problem because (a) it was intermittent and (b) it frequently happened after a connection was closed. Maybe an object was getting deleted during marking?

The only thing that was weird was that the bug didn't happen under stress (I tried stress testing the system, but couldn't reproduce it). In fact, it seemed to happen most often at startup, when there weren't too many connections or threads running.

Eventually I proved to myself that all threads were paused properly during marking. And with sufficient logging, I proved that an object was not being deleted during marking, but the marking thread crashed anyway.

[Quick aside: I tried to get ChatGPT to help--o3 pro--and it kept on suggesting a concurrency problem. I could never really convince it that all threads were stopped. It always insisted on adding a lock around marking to protect it against other threads.]

The one thing I didn't consider was that maybe an object was not getting marked properly and was getting deleted even though it was still in use. I didn't consider it because the crash was in the marking code! Clearly we're marking objects!

But of course, that was the bug. Looking at the code I saw that an object was marked by a connection but not by the listener it belonged to. That meant that, as long as there was a connection active, everything worked fine. But if ever there were no connections active, and if we waited a sufficient amount of time, the object would get deleted by GC because the listener had forgotten to mark it.

Then a connection would use this stale object and on the next marking pass, it would crash.

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

#32

Post by sitkack »

ngruhn wrote: post #28
bcheung wrote: post #26

I wonder how many of these rules can be incorporated into a linter or be evaluated by an LLM in an agentic feedback loop. It would be nice to encourage code to be more like this. I notice you didn't really talk much about types. When I think of proofs in code my mind goes straight to types because they literally are proofs. Richer typed languages move even more in that direction. One caveat I would add is it is not a…

Sorry for being pedantic but isn't the story that types=theorems and programs=proofs?

"Propositions as Types" by Philip Wadler https://www.youtube.com/watch?v=IOiZatlZtGU

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

#33

Post by phkahler »

taeric wrote: post #24

I feel like this is reaching for the vocabulary that you get in mathematics of axioms, postulates, and theorems. Not in a bad way, mind. Just the general idea of building a separate vocabulary for the different aspects of a system of knowledge. I also think things get complicated with holding things constant as a necessity. Often times, the best way to find a bug is to ask not "how was this possible?" but "why would…

Another nice pattern is to have any particular value written exactly once, or from exactly one place in the code if it gets updated.

For embedded control I'm finding the blackboard pattern with single assignment to be super useful.

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

#34

Post by sitkack »

nayuki wrote: post #7

I 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…

Those notes are great, David Liu seems while a wholesome dude https://www.cs.toronto.edu/~david/research.html

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

#35

Post by fragmede »

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…

A research paper from Google in 2006 noted that "almost all" binary search (and merge sort) implementations contain a bug (and had for decades), so 90% seems impressive in the face of that.

https://research.google/blog/extra-extra-read-all-about-it-n...

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

#36

Post by msteffen »

bluetomcat wrote: post #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…

I think your frustration is illustrative, actually: the reason mutable global state is bad is because in order to prove that a piece of code reading it is correct, you have to know what _the entire rest of the program_ is doing.

If, instead, you make the global variable immutable, make the state variable into a function argument, or even wrap the mutable global state in some kind of helper class, then you only need to know what the callers of certain functions are doing. The visibility of those functions can be limited. Caller behavior can be further constrained with assertions inside the function. All of these (can) make it easier to prove that the reader is correct.

I think most programmers already do this, actually; they just don't think of their decisions this way.

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

#37

Post by gregorygoc »

wizzwizz4 wrote: post #6
gregorygoc wrote: post #4

Writing 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.

No, appropriate abstractions are insufficient for my argument. For example: there’s one way to write an idiomatic loop in C and it inherits necessary invariants by construction.

I highly recommend reading the book, it explains concept of writing idiomatic code way better than I ever could.

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

#38

Post by hiAndrewQuinn »

fragmede wrote: post #35
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…

A research paper from Google in 2006 noted that "almost all" binary search (and merge sort) implementations contain a bug (and had for decades), so 90% seems impressive in the face of that. https://research.google/blog/extra-extra-read-all-about-it-n...

The bug in that paper is actually the very buffer overflow bug I was referring to. Given that Jon himself made that error in the "definitive" implementation, it seems unlikely that he would have spotted it in the 10% of implementations he considered correct. Under Google's stricter criteria it seems likely to me that not a single person got the search implementation truly correct enough.

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

#39

Post by pokemyiout »

Is there a typo in the induction section? Should `simplifyTree` and `simplifyGraph` be the same function?

function simplifyTree(root: Node): Node {

  let newChildren = [] as Array;

  for (const child of root.children) {
    const simplifiedChild = simplifyGraph(child);
  
    if (shouldContract(simplifiedChild)) {
      for (const grandChild of simplifiedChild.children) {
        newChildren.push(grandChild);    
      }
    } else {
      newChildren.push(simplifiedChild);
    }
  }

  root.children = newChildren;

  return root;
}

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

#40

Post by sedatk »

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…

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.
Post reply on HN