5 ms·
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-pos
by gregorygoc 1y ago
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 in a day job.
On a slightly related note… Competitive programming is surprisingly good at teaching you the right set of techniques to make sure your code is correct. You won’t progress beyond certain stage unless you pick them up.
- wizzwizz4 1y agoTurn 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.
- gregorygoc 1y agoNo, 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.
- chowells 1y agoThat'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 <= j? What does that loop do when j is INT_MAX?
- wk_end 1y agoI 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!
- chowells 1y agoYeah, it's a hard case in general. But C's idioms really don't encourage you to think about it. You really need to default to a loop structure that checks the termination condition after the loop body but before the increment operation for inclusive end coordinates. It's easy to think that's what do/while is for, but it turns out to be really hard to do the increment operation after the conditional, in general. What you really want is a loop structure with the conditional in the middle, and the only general purpose tool you get for that is a break. C (or any language with similar syntax) really doesn't have an idiom for doing this correctly.
- wizzwizz4 1y agoThis may be hubris, but… int i = start; do thing_with(i) while (i++ <= end);
- chowells 1y agoI did consider that, but I wrote "in general" for a reason. It works very specifically in the case of "add one" or "subtract one", but it doesn't work with anything more complicated, like chasing pointers or adding/subtracting more than one at a time. You could write functions to do the update and return the old value so you could use them in the same way, but I don't like this either. This is mostly because it orders the termination check and the update logic the wrong way around. If there's IO involved in checking for the next thing, for example, side effects of that unnecessary operation might interfere with other code. You could resolve that by moving the termination check into the update logic as well, but now you're seriously complecting what should be independent operations. I don't think the tradeoff is there versus just using a break. But mostly, this is a self-inflicted problem in C's language constructs and idioms. I just don't have this problem in many other languages, because they provide end-inclusive looping constructs.
- xg15 1y agoHave 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.
- mprast 1y agoyes, what i had in mind were more proof sketches than proofs
- smohare 1y ago[dead]
- Nevermark 1y agoYes, 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.
- Sharlin 1y agoTypes 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.
- gregorygoc 1y agoYeah, and I’m saying if your code is idiomatic you get necessary invariants for free.
- auggierose 1y agoIs idiomatic related to idiotic?
- bmn__ 1y ago
- pipes 1y agoCould you elaborate on those techniques from competitive programming please. Genuinely interested! :)
- kevinventullo 1y ago+1 This is definitely the wall I hit with competitive programming. I logically know how to solve the problem, my code just ends up having one too many bugs that I can’t track down before time is up.
- mathgradthrow 1y agoThere is no substitute for writing correct programs, no matter how hard it is. If you want correct programs you have to write them correctly.
- monkeyelite 1y agoThe 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.
- maxbond 1y agoI think the causality is flipped here, when you carefully consider a problem the result is often very clean and clear code. The clarity in your thinking is reflected in the code and it's structure. But writing clean and clear code in the hopes that it's good aesthetics will result in correctness would be cargo culting. (Writing clean code is still worthwhile of course, and clean code + code review is likely to result in better correctness.) Form follows function, not the other way around.