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

71–80 of 181 posts

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

#71

Post by swat535 »

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…

TDD is also great for playing around with ideas and coming up with a clean interface for your code. It also ensures that your code is testable, which leads to improved readability.

You'll know quickly where you're going wrong because if you struggle to write the test first, it's a symptom of a design issue for example.

That being said, I wouldn't use it as dogma, like everything else in CS, it should be used at the right time and in the right context.

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

#73

Post by saurik »

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…

A test is not a proof, and you can prove something works without ever even running it. There are also properties of a system which are impossible to test, or are so non-deterministic that you a test will only fail once every million times the code is executed. You really need to just learn to prove stuff.

The most complex piece of code I have ever written, as a relevant story, took me a month to prove to everyone that it was correct. We then sent it off to multiple external auditors, one of which who had designed tooling that would let them do abstract interpretation with recursion, to verify I hadn't made any incorrect assumptions. The auditors were confused, as the code we sent them didn't do anything at all, as it had a stupid typo in a variable name... I had never managed to figure out how to run it ;P. But... they found no other bugs!

In truth, the people whom I have met whom are, by far, the worst at this, are the people who rely on testing, as they seem to have entirely atrophied the ability to verify correctness by reading the code and modeling it in some mathematical way. They certainly have no typos in their code ;P, but because a test isn't a proof, they always make assumptions in the test suite which are never challenged.

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

#74

Post by pclowes »

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

TDD is also great for playing around with ideas and coming up with a clean interface for your code. It also ensures that your code is testable, which leads to improved readability. You'll know quickly where you're going wrong because if you struggle to write the test first, it's a symptom of a design issue for example. That being said, I wouldn't use it as dogma, like everything else in CS, it should be used at the r…

I agree on the Dogma aspect. Plenty of times I have abandoned it. However, I did find it very helpful to spend my first couple years in a strict Xtreme Programming (XP) shop. The rigor early on was very beneficial and its a safety net for when I feel out of my depth in an area.

I tend to go the other way, I don't use TDD when I am playing around/exploring as much as when I am more confident in the direction I want to go.

Leaving a failing test at the end of the day as a breadcrumb for me to get started on in the morning has been a favored practice of mine. Really helps get the engine running and back into flow state first thing.

The dopamine loop of Red -> Green -> Refactor also helps break through slumps in otherwise tedious features.

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

#75

Post by monocasa »

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

> 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. I think this reinforces the article's point. Code like this is much more likely to contain bugs and be harder to maintain without introducing more bugs, than programs written from the outset with this goal of "provability".

And in fact, when you look at formally proven code, 80% of the shtick is reducing complexity of mutation to something tractable. That's valuable whether or not you then actually go through the process of formally proving it.

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

#76

Post by init1 »

Instead of just thinking about the proof in your mind or putting it in comments you can actually embed pre/post conditions and compile time proofs in actual code using ADA SPARK. You use Pre and Post aspects for subprograms and pragma Invariant for loops and such constructs. The spark toolchain will run provers against your code and show if it can show the proofs hold.

https://www.youtube.com/watch?v=tYAod_61ZuQ

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

#77

Post by pclowes »

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

A test is not a proof, and you can prove something works without ever even running it. There are also properties of a system which are impossible to test, or are so non-deterministic that you a test will only fail once every million times the code is executed. You really need to just learn to prove stuff. The most complex piece of code I have ever written, as a relevant story, took me a month to prove to everyone tha…

Interesting, could you show me a formal proof that can't be expressed in logic (ie. code) and then tested?

My thought here is that since proofs are logic and so is code you can't have a proof that can't be represented in code. Now admittedly this might look very different than typical say JUnit unit tests but it would still be a test validating logic. I am not saying every system is easily testable or deterministic but overall, all else equal, the more tested and testable a system is the better it is.

IME things that are very hard to test are often just poorly designed.

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

#78

Post by monkeyelite »

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 C++ standard library phrases binary search as a partitioning problem - finding the index where a predicate goes from false to true, which is helpful for me.

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

#79

Post by GuB-42 »

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 thing. Like throwing stuff at your tests and see what sticks.

I much prefer the traditional approach of first solving the problem the best you can, which may of may not involve thinking about invariants, but always with the end result in mind. And only when you are reasonably confident with your code, you can start testing. If it fails, you will have the same temptation to just pass the test, but at least, you wrote it at least once without help from the tests.

Maybe that's just me, but when I tried the "tests first" approach, the end result got pretty bad.

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

#80

Post by monkeyelite »

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…

The most basic idea of a proof is an argument for why something is true. It’s not about avoiding small mistakes, it’s about getting directionally correct.
Post reply on HN