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

41–50 of 181 posts

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

#41

Post by gregorygoc »

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.

Yeah, and I’m saying if your code is idiomatic you get necessary invariants for free.

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

#42

Post by dkenyser »

This reminds me of reading Accelerated C++ back in the day and I think the part that stuck with me most from that book was the idea of "holding the invariant in your head" (I'm paraphrasing a bit).

It made me think a lot more about every line of code I wrote and definitely helped me become a better programmer.

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

#44

Post by TacticalCoder »

GMoromisato wrote: post #31

Totally tangential, but I love to read post-mortems of people fixing bugs. What were the initial symptoms? What was your first theory? How did you test it? What was the resolution? Raymond Chen does this a lot and I've always enjoyed it. I learn more from these concrete case studies than from general principles (though I agree those are important too). One of my most recent bugs was a crash bug in a thread-pool that…

> Totally tangential, but I love to read post-mortems of people fixing bugs.

I know I already posted it moons ago but... Around 1991 I made a little game, similar to Canon Ball on the MSX (which later on Pang / Buster Bros did copy).

I had one weird case where sometimes the game would crash. Plain crash. But sometimes after playing for 15 minutes and already passing several levels. I just couldn't find it. I couldn't reason about it. I was stuck.

So I decided to rewrite not the entire game but the part dealing with the inputs / game logic to make it 100% deterministic. It took me a long time to do that. Then eventually I could record myself playing: I've record only the player inputs and at which moment they'd happen, which would make for tiny savefiles btw.

And eventually while I was playing and recording, the crash occured. I tried my replay: it worked... It replayed the savefile flawlessly and the game crashed again.

At that point I knew the bug was gone: being able to reproduce a bug in a deterministic way means I was going to fix it.

Turns out it was a dangling pointer (ah, C...): when the hero would catch an extra allowing him to fire two shots at once on screen (usually he'd only be allowed one) and would the first shot kill the last ball on screen, then on the next level the second shot would somehow (due to an error on my part) continue to live its live, eventually corrupting memory.

Fun stuff.

FWIW having deterministic game engines wasn't a thing back then. It became common later on, with games like Age of Empires and Warcraft III etc. using them: it was obvious for savefiles allowing to replay/exchangs games were tinier than tiny: they'd only save at which frame a player input happened and they'd replay the entire game from there [1]

I still have the code to that game, it was surprisingly fun. Someone here already offered help in the past to get it back on its feet. I've also got an executable that runs. I just don't remember how the tooling worked. Still have the BAT files etc. to build it, but not the tools. I really should look into that one of these days but I'm kinda busy with other projects / life.

[1] which also raised another issue: when game engines were upgraded, you could have savefiles only playing on older version of the game, so players would exchanges games and add the version of the game they were destined to

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

#45

Post by bluetomcat »

msteffen wrote: post #36
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…

I think your frustration is illustrative, actually: the reason mutable global state is bad is because in order to prove that a piece of code reading it is correct, you have to know what _the entire rest of the program_ is doing. If, instead, you make the global variable immutable, make the state variable into a function argument, or even wrap the mutable global state in some kind of helper class, then you only need t…

It’s a good direction to follow, but it can only get you so far. Some pieces of code do naturally evolve into a functional formalism, while others are inherently imperative. Usually, the top levels of your program (event loop) are imperative and deal with stateful “devices” like IO, the screen and storage subsystems. The “leaf” functions from the call graph can be functional, but you still can’t reason about the whole program when it is imperative at the top.

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

#47

Post by mathgradthrow »

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…

There is no substitute for writing correct programs, no matter how hard it is. If you want correct programs you have to write them correctly.

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

#48

Post by wrs »

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.

Post reply on HN