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

21–30 of 181 posts

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

#21

Post by Nevermark »

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.

Yes, we could call this “maintaining plausible provability”.

Code for which there is not even a toehold for an imagined proof might be worth cordoning off from better code.

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

#22

Post by trealira »

roadside_picnic wrote: post #10

What's interesting about this view is that theorem provers ultimately boil down to sufficiently advanced type checking (the book Type Theory and Formal Proof is an excellent overview of this topic). Literally the heart of proof assistants like Lean is "if it compiles, you've proved it". So more practical type systems can be viewed as "little" theorem provers in the sense the author is describing. "Thinking in types"…

It's true that theorem provers can be just sufficiently advanced type systems (the Curry Howard correspondence), but not all theorem provers operate that way. Isabelle/HOL operates on higher order logic. Imperative ones like SPARK or Dafny just rely on encoding preconditions and postconditions and things like loop invariants and just use SMT solvers for verification, IIRC.

Having an advanced type system does seem to encourage this sort of informal proof oriented thinking more than imperative and somewhat typeless languages do, though, since preconditions and postconditions and loop invariants and inductive proofs on loops are things you have to do yourself entirely in your head.

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

#23

Post by cespare »

I really identify with this way of thinking. One domain where it is especially helpful is writing concurrent code. For example, if you have a data structure that uses a mutex, what are the invariants that you are preserving across the critical sections? Or when you're writing a lock-free algorithm, where a proof seems nearly required to have any hope of being correct.

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

#24

Post by taeric »

I feel like this is reaching for the vocabulary that you get in mathematics of axioms, postulates, and theorems. Not in a bad way, mind. Just the general idea of building a separate vocabulary for the different aspects of a system of knowledge.

I also think things get complicated with holding things constant as a necessity. Often times, the best way to find a bug is to ask not "how was this possible?" but "why would another part of the system modify this data?"

Obviously, if you can make things reference capable data, you should do so. But, all too often "this data being X" has a somewhat self evident explanation that can help. And just "copy so I don't have to worry about it" lands you squarely in "why is my copy out of date?"

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

#25

Post by xg15 »

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…

Even then, you can get a map of "safe" and "unsafe" locations in the codebase, I.e. you can get a mental model of which functions modify global state and which don't.

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

#26

Post by bcheung »

I wonder how many of these rules can be incorporated into a linter or be evaluated by an LLM in an agentic feedback loop. It would be nice to encourage code to be more like this.

I notice you didn't really talk much about types. When I think of proofs in code my mind goes straight to types because they literally are proofs. Richer typed languages move even more in that direction.

One caveat I would add is it is not always desirable to be forced to think through every little scenario and detail. Sometimes it's better to ship faster than write 100% sound code.

And as an industry, as much as I hate it, the preference is for languages and code that is extremely imperative and brittle. Very few companies want to be writing code in Idris or Haskell on a daily basis.

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

#27

Post by bcheung »

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.

The problem is the training corpus tends towards mediocre code. But with an agentic loop that analyzes the code against those criteria and suggests changes then I think it might be possible. I wouldn't try to get it to generate that right off the bat.

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

#28

Post by ngruhn »

bcheung wrote: post #26

I wonder how many of these rules can be incorporated into a linter or be evaluated by an LLM in an agentic feedback loop. It would be nice to encourage code to be more like this. I notice you didn't really talk much about types. When I think of proofs in code my mind goes straight to types because they literally are proofs. Richer typed languages move even more in that direction. One caveat I would add is it is not a…

Sorry for being pedantic but isn't the story that types=theorems and programs=proofs?

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

#29

Post by Sharlin »

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.

Types constitute this sort of a partial proof. Not enough to encode proofs of most runtime invariants (outside powerful dependent type systems) but the subset that they can encode is extremely useful.

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

#30

Post by Nevermark »

mprast wrote: post #15
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.

I was thinking the same thing!

In any other industry the “worker class” would be sabotaging the machines.

In the merry software world, the challenges of improving our potential replacements are far too interesting and satisfying to leave room for any worry about consequences! :)

Post reply on HN