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

121–130 of 181 posts

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

#121

Post by ericmcer »

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…

This made me think how I constantly rethink my approach to coding and learning how to do it “right” over and over.

I wonder if someone like a John Carmack is just like… yeah I got it or he also is constantly feeling like he was bad 5 years ago and is doing it “better” now.

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

#122

Post by gitremote »

GuB-42 wrote: post #79
pclowes wrote: post #66

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

I am not a fan of Test Driven Development, not at all. Having your invariants and pre/post conditions correct is not enough. You also need to do the right thing. For example, you have a function that adds two durations in the form hh:mm:ss, you have mm Problem is, when you write tests first, especially tight, easy to run unit tests, you will be tempted to write code that pass the tests, not code that does the right t…

I do TDD and write proofs as tests. TDD practitioners never said TDD is a substitute for thinking.

> Problem is, when you write tests first, especially tight, easy to run unit tests, you will be tempted to write code that pass the tests, not code that does the right thing. Like throwing stuff at your tests and see what sticks.

I never had that problem, but I knew how to code before I started TDD.

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

#123

Post by atlintots »

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…

UofT mentioned! Let's go!

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

#124

Post by jansan »

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

In Javascript that Google "bug" only occurs if an array has more than 4503599627370495 items. You may run into memory issues before running into that bug.

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

#125

Post by edanm »

sedatk wrote: post #40
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.

Oh interesting, where can we read about the bug that was there?

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

#126

Post by trealira »

chowells wrote: post #108
wizzwizz4 wrote: post #104

Earlier quoted context omitted.

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

I did consider that, but I wrote "in general" for a reason. It works very specifically in the case of "add one" or "subtract one", but it doesn't work with anything more complicated, like chasing pointers or adding/subtracting more than one at a time. You could write functions to do the update and return the old value so you could use them in the same way, but I don't like this either. This is mostly because it order…

> I did consider that, but I wrote "in general" for a reason. It works very specifically in the case of "add one" or "subtract one", but it doesn't work with anything more complicated, like chasing pointers or adding/subtracting more than one at a time.

You're reminding me of the book "Modern Compiler Design." The author goes over how to compile a general Pascal-style for-loop correctly, accounting for increasing or decreasing ranges, differing step sizes, and accounting for overflow. It was written using just goto statements, so I adapted a version of it to C. Just replace "intN_t" with an actual integer size. It works by calculating the number of times the loop will run. If "from" is equal to "to," it's still going to run at least once. Again, this is not mine, just adapted from the author's code (Dick Grune's).

  // enumerate: print out numbers from "from" to "to", inclusive, with step size "by"
  void enumerate(intN_t from, intN_t to, intN_t by) {
      uintN_t loop_count;
      intN_t i;
      if (by > 0) {
          if (from > to) return;
          loop_count = (to - from) / by + 1;
      } else if (by
You can see it's more complicated than the idiomatic C for-loop, haha. But that's just a general solution. Like you guys noted, it could be simpler for step sizes of 1.

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

#128

Post by graycat »

Maybe a related practice (what I do): Write actual proofs or good documentation that contains essentially proofs and combine that with Knuth's Literate programming.

For what is to be proved, try to use divide and conquor to make the whole proof consist of separate steps, each of which gets a short proof and each of those steps might become a subroutine (whatever the terminology and functionality of the programming language and environment).

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

#130

Post by saghm »

begueradj wrote: post #127

> sketch a proof in your head as you go that your code will actually do what you want it to do. Could anyone, please, explain me the meaning ? I can't get it.

Everyone writes code that has bugs in it, but no one intends to write code that has bugs. The bugs occur because there's a disparity between what you think your code is doing and what your code is actually doing. The quote you give is an suggestion for how to reduce how often this occurs by considering why you should be confident about your intent being properly conveyed by the code you've written.

It might help to think of this almost as debugging your program as you write it rather than only after you run it. Debugging a program is essentially the same process of trying to figure out why the program isn't doing what you think of doing. While there's information you can get by inspecting a running program or its outputs, there's often some amount of consideration you need to do in order to figure out why you think certain behavior might be happening. There's no fundamental reason this consideration can't happen before you actually run the program; even as you're writing the code, you can think about all the ways it could potentially go wrong, and why you're confident that this isn't the case. If you can't come up with a strong argument for that, it's a good sign you might need to reconsider your approach!

Post reply on HN