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.
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.
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.
Yeah, and I’m saying if your code is idiomatic you get necessary invariants for free.
I bought The Practice of Programming years ago. It's a great book that is no less relevant today, but I don't see your argument. The suggestions you've summarized are critical advice, but rather than obviate the need for the proof-like mindset, they complement it. Idiomatic code doesn't directly help you solve and implement difficult algorithmic or architectural problems. However, idiomatic code certainly helps reduce noise so that the irreducibly complex aspects of a solution conveniently standout, both conceptually and literally.
I do agree they do complement each other… to some extent. My point was rather that if you write a good code, keeping logical arguments in your head should be reduced to the minimum. To the point that only testing edge cases and a happy path in your mind should be sufficient.
To give a more concrete example: I have recently seen a very complicated piece of logic checking whether a subsequent code should be even invoked, but it was hidden in a debris of core logic and other verification. It easily could have been separated and rewritten as a series of early returns and this is what a precondition is. I’m sure someone who wrote the code had it in their mind but was not familiar enough with the early return technique to embed this in code. Had they been, their brain power could’ve been utilized more efficiently.
Is idiomatic related to idiotic?
People downvoted you because instead of polluting the discussion, you could have looked this up yourself.
The answer is yes, both words are related to idios, "own", "self", "private".
Please don't comment about the voting on comments. It never does any good, and it makes boring reading.
https://news.ycombinator.com/newsguidelines.html
yes, what i had in mind were more proof sketches than proofs
[dead]
I 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.
The 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.
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.
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 <= j?
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!
Yeah, 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.
This may be hubris, but…
I 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.
> I 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're reminding me of the book "Modern Compiler Design." The author goes over how to compile a general Pascal-style for-loop correctly, accounting for increasing or decreasing ranges, differing step sizes, and accounting for overflow. It was written using just goto statements, so I adapted a version of it to C. Just replace "intN_t" with an actual integer size. It works by calculating the number of times the loop will run. If "from" is equal to "to," it's still going to run at least once. Again, this is not mine, just adapted from the author's code (Dick Grune's).
You can see it's more complicated than the idiomatic C for-loop, haha. But that's just a general solution. Like you guys noted, it could be simpler for step sizes of 1.Could you elaborate on those techniques from competitive programming please. Genuinely interested! :)
+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.