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

141–150 of 181 posts

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

#141

Post by MoreQARespect »

GuB-42 wrote: post #88
JohnKemeny wrote: post #83

Earlier quoted context omitted.

You’ve missed the most important point of TDD—and indeed, of tests. Tests do not ensure that your functions are correct; they ensure that you are alerted when their behavior changes. Second, TDD is a way to force dogfooding: having to use the functions you’re going to write, before you write them, helps you design good interfaces.

> Tests do not ensure that your functions are correct; they ensure that you are alerted when their behavior changes. I agree with that part and I am not against tests, just the idea of writing tests first. > helps you design good interfaces I am sure plenty of people will disagree but I think testability is overrated and leads to code that is too abstract and complicated. Writing tests first will help you write code…

>It makes sense at a high level though

This is the way I've always done TDD.

I don't think it makes sense to do it any other way. If a test case doesn't map on to a real scenario you're trying to implement the code for it doesn't make any sense to write it.

I find that people who write the test after tend to miss edge cases or (when they're trying to be thorough) write too many scenarios - covering the same code more than once.

Writing the test first and the code that makes it pass next helps to inextricably tie the test to the actual code change.

>but it is not always possible

I don't think I've written any production code in years where I gave up because it was intrinsically not possible.

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

#142

Post by bmn__ »

w3news wrote: post #139

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

The five properties used as headings in the article are able to be expressed in good type systems. This way a huge part of the specification becomes code, and the compiler guarantees to uphold the expressed properties in many or all cases. We should strive to have a programming future where this idea is normal and commonplace.

OpenAPI and GraphQL have exceedingly poor types, and will not bring us there unless they make a fifty year leap forward.

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

#143

Post by shahzaibmushtaq »

Almost every programmer gets better through their own trial and error.

For me, the best "trick" is to start with pseudocode.

The Isolation part is understandable and supports the philosophy:

> When requirements change, you extend the behavior of [your program] by adding new code, not by changing old code that already works.

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

#144

Post by mdnahas »

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 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 0 and R to n-1”. That is, R is an inclusive bound. But we’ve learned that for most string algorithms, it is better when your upper bound is an exclusive bound, that is, n.

I’ve wanted to do an experiment testing that hypothesis. That is, ask a large number of people to write it with different function prototypes and initial calls and see how many buggy implementations I get with inclusive vs exclusive upperbound vs length.

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

#146

Post by n4r9 »

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

What are the odds you write a binary search that you'll use more than once instead of just running it and writing down the result?

I have an object representing piecewise linear functions, defined by a sequence of (x_i, y_i) tuples. It has a method to evaluate y for a given value of x. The first step is to find the least i for which x_i is greater than or equal to x: this uses a binary search. Initially, I stored the x values in a separate array and used dotnet's inbuilt Array.BinarySearch. Later I removed this array to save on memory and it now runs a handbuilt binary search on the first items of the array of points instead.

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

#147

Post by [deleted] »

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…

[deleted]

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

#148

Post by purplesyringa »

Animats wrote: post #3

Now if we can get LLMs to do that, they might code better. Proofs are a lot of work, but might keep LLMs on track.

IME, LLMs are completely incapable of reasoning about anything remotely difficult. All you'll get are proofs by assertion, not anything rigid you can trust.

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

#149

Post by gregorygoc »

wahern wrote: post #135
gregorygoc wrote: post #41

Earlier quoted context omitted.

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

I do agree they do complement each other… to some extent. My point was rather that if you write a good code, keeping logical arguments in your head should be reduced to the minimum. To the point that only testing edge cases and a happy path in your mind should be sufficient.

To give a more concrete example: I have recently seen a very complicated piece of logic checking whether a subsequent code should be even invoked, but it was hidden in a debris of core logic and other verification. It easily could have been separated and rewritten as a series of early returns and this is what a precondition is. I’m sure someone who wrote the code had it in their mind but was not familiar enough with the early return technique to embed this in code. Had they been, their brain power could’ve been utilized more efficiently.

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

#150

Post by auggierose »

bmn__ wrote: post #140
auggierose wrote: post #53

Earlier quoted context omitted.

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

Please don't comment about the voting on comments. It never does any good, and it makes boring reading.

https://news.ycombinator.com/newsguidelines.html

Post reply on HN