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

Post by pipes » Tue, Jul 15, 2025, 6:14 PM UTC

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…

Post by akavi » Tue, Jul 15, 2025, 6:17 PM UTC

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…

Post by mprast » Tue, Jul 15, 2025, 6:19 PM UTC

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.

Post by mprast » Tue, Jul 15, 2025, 6:21 PM UTC

xg15 wrote: post #8

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…

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.

Post by mprast » Tue, Jul 15, 2025, 6:23 PM UTC

akavi wrote: post #13

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…

A part of "being a good developer" is being able to evolve systems in this direction. Real systems are messy, but you can and should be thoughtful about: 1. Progressively reducing the number of holes in your invariants 2. Building them such that there's a pit of success (engineers coming after you are aware of the invariants and "nudged" in the direction of using the pathways that maintain them). Documentation can he…