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

51–60 of 181 posts

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

#51

Post by chowells »

gregorygoc wrote: post #37
wizzwizz4 wrote: post #6

Earlier quoted context omitted.

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.

That's a really funny example, given how many bugs have been found in C programs because idiomatic loops are wrong in the edge cases.

How do you idiomatically write a loop to iterate over signed ints from i to j (inclusive) in increasing order, given i What does that loop do when j is INT_MAX?

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

#52

Post by AIPedant »

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.

Most proof assistants do a good job with autogenerating a (deterministically correct) proof given a careful description of the theorem. Working on integrating this into mainstream languages seems much more worthwhile than training an LLM to output maybe-correct proof-seeming bits of text.

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

#53

Post by auggierose »

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.

Is idiomatic related to idiotic?

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

#54

Post by jimbokun »

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

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

#55

Post by jimbokun »

xg15 wrote: post #12

I'd also add mutability and immutability to the list of properties. Keeping as much state as possible immutable doesn't just help with multithreading, it will also greatly reduce the headache when trying to understand the possible states of a program.

The article does include those.

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

#56

Post by wk_end »

chowells wrote: post #51
gregorygoc wrote: post #37

Earlier quoted context omitted.

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.

That's a really funny example, given how many bugs have been found in C programs because idiomatic loops are wrong in the edge cases. How do you idiomatically write a loop to iterate over signed ints from i to j (inclusive) in increasing order, given i What does that loop do when j is INT_MAX?

I can imagine someone who sketches out little proofs in their head - or even on paper - missing that case too. It’s easy to forget you’re not doing normal arithmetic when doing arithmetic in C!

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

#57

Post by tristramb »

The idea that you should design programs with proof in mind goes back to T. J. Dekker's solution to the mutual exclusion problem in 1959. The story is told by Edgser Dijkstra in EWD1303 (https://www.cs.utexas.edu/~EWD/transcriptions/EWD13xx/EWD130...). Much of Dijkstra's later work can be seen as him working out the consequences of this insight.

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

#58

Post by thesuperbigfrog »

Why not include little proofs in the code when you can?

Several programming languages and libraries support Design-by-Contract (https://en.wikipedia.org/wiki/Design_by_contract) which lets you specify preconditions, postconditions, and invariants directly in your code.

Those predicates can be checked in various ways (depending on how deeply Design-by-Contract is supported) to help you know that your code is working correctly.

Ada supports Design-by-Contract as part of the language: https://learn.adacore.com/courses/intro-to-ada/chapters/cont...

SPARK extends Ada Design-by-Contract into full proofs: https://learn.adacore.com/courses/intro-to-spark/index.html

Rust has the Contracts crate: https://docs.rs/contracts/latest/contracts/

Other programming languages have various levels of support or libraries for Design-by-Contract: https://en.wikipedia.org/wiki/Design_by_contract#Language_su...

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

#59

Post by bigmadshoe »

thesuperbigfrog wrote: post #58

Why not include little proofs in the code when you can? Several programming languages and libraries support Design-by-Contract ( https://en.wikipedia.org/wiki/Design_by_contract ) which lets you specify preconditions, postconditions, and invariants directly in your code. Those predicates can be checked in various ways (depending on how deeply Design-by-Contract is supported) to help you know that your code is working…

Even standard assertions work as a version of this

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

#60

Post by TheShermanTank »

wrs wrote: post #48

As an undergrad at Carnegie Mellon in the 80s, I was explicitly taught to do all of these things in one of the first-year programming courses. And it has served me very well since then. I especially remember how learning the equivalence of recursion and induction immediately eliminated the “frustrated trial and error” approach for making recursive algorithms that work.

Took the course last year, and I started to appreciate it more while taking functional programming lmao
Post reply on HN