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

131–140 of 181 posts

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

#131

Post by scuol »

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 way I always remember leftmost and rightmost binary search (the C++ equivalents-ish of lower_bound and upper_bound) is to always have a "prior best" and then move the bounds according to the algo

while (l {

//find the midpoint

auto mp = l + (l-r)/2;

if (nums[mp] == target) { prior = target;

#ifdef upper_bound

l = target + 1; // move the left bound up, maybe there's more up there we can look for!

#else

//lower bound, we found the highest known instance of target, but let's look in the exclusive left half a bit more

r = target - 1;

#endif

}

excuse the terrible formatting, it's been a long day grinding leetcode after getting laid off...

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

#132

Post by begueradj »

saghm wrote: post #130
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 t…

It makes sense. Thank you for the effort.

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

#133

Post by saghm »

ericmcer wrote: post #121
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.

This is an important point I like to mention to people. Thinking back to old code you wrote and how you would choose to do it better than you originally did it a sign of growth, and if that stops happening after a certain point, it's a sign you've stopped growing. Given that the best programmers in the world still don't write perfectly bug-free code, I don't have any illusions that there will always be plenty of room for me to continue improving as a programmer, so I consider having those thoughts to be an unequivocally good thing. I'd honestly be a bit wary of anyone who didn't think they needed to learn or grow any more as a programmer!

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

#134

Post by hiAndrewQuinn »

scuol wrote: post #131
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 way I always remember leftmost and rightmost binary search (the C++ equivalents-ish of lower_bound and upper_bound) is to always have a "prior best" and then move the bounds according to the algo while (l { //find the midpoint auto mp = l + (l-r)/2; if (nums[mp] == target) { prior = target; #ifdef upper_bound l = target + 1; // move the left bound up, maybe there's more up there we can look for! #else //lower bou…

Godspeed, fellow LeetCoder. I'm not currently grinding but I still have my handful of practice problems in active Anki rotation.

I have my rightmost code at part III of the miniseries, [1]. It loks quite similar, but I save the -1 for the very end return.

    def rightmost_bsearch(L, T):
      l, r = 0, len(L)

      while l  T

        mid = (l + r) // 2

        if L[mid] > T:
          r = mid
        else:
          l = mid + 1

      return r - 1 # return the first element AFTER L[r:len(L)].
(It should technically be BEFORE, I guess. If it helps all rightmost bsearches are also leftmost bsearches on the reversed array, so AFTER is secretly not wrong)

[1]: https://hiandrewquinn.github.io/til-site/posts/binary-search...

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

#135

Post by wahern »

gregorygoc wrote: post #41
xg15 wrote: post #8

Earlier quoted context omitted.

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.

Yeah, and I’m saying if your code is idiomatic you get necessary invariants for free.

I bought The Practice of Programming years ago. It's a great book that is no less relevant today, but I don't see your argument. The suggestions you've summarized are critical advice, but rather than obviate the need for the proof-like mindset, they complement it. Idiomatic code doesn't directly help you solve and implement difficult algorithmic or architectural problems. However, idiomatic code certainly helps reduce noise so that the irreducibly complex aspects of a solution conveniently standout, both conceptually and literally.

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

#137

Post by godelski »

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…

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 usage and test cases if __name__ == "__main__": # Test cases test_array = [1, 3, 5, 7, 9, 11, 13, 15]

    print(binary_search(test_array, 7))    # Output: 3
    print(binary_search(test_array, 1))    # Output: 0
    print(binary_search(test_array, 15))   # Output: 7
    print(binary_search(test_array, 4))    # Output: -1
    print(binary_search([], 5))            # Output: -1
    print(binary_search([5], 5))           # Output: 0
    print(binary_search([5], 3))           # Output: -1

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

#138

Post by hiAndrewQuinn »

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

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 overflow and produce undefined behavior; in practice it usually gives you I think -2^63, which is obviously going to screw up the bsearch a bit. It isn't wrong, just slightly less idiomatic for the language.

Python's interpreter may or may not be able to recognize and refactor the slight inefficiency of the extra arithmetic operation out. I will only point out that most of the time when we write our own bsearch it's because we want to optimize something really fundamental to the codebase. Any time you have to whip up your own algorithm it's prima facie evidence that that part of the code might be good to profile.

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

#139

Post by w3news »

To be a better programmer, write little proofs in your code. We call that tests and types, proof that it should do what you expect. Especially when writing tests first, then types, then the code. Start with a test per acceptance criteria, that well describes what it should do, and is clear what you send and receive. Also in an API you can describe the API in OpenAPI or GraphQL with all the properties and types, and you can validate on runtime the data on your specification, that specification is than also a proof that the application does what you described in your specification.

So OpenAPI/GraphQL, tests and types and proof that the system works like intended. Always start with that before writing code. The specification is a solid base that doesn't change a lot if you start with it. How the code works, you can refactor it, and proof with the specification if it sill does the same like before.

Code is less important than the specifications.

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

#140

Post by bmn__ »

auggierose wrote: post #53
gregorygoc wrote: post #41

Earlier quoted context omitted.

Yeah, and I’m saying if your code is idiomatic you get necessary invariants for free.

Is idiomatic related to idiotic?

People downvoted you because instead of polluting the discussion, you could have looked this up yourself.

The answer is yes, both words are related to idios, "own", "self", "private".

Post reply on HN