To be a better programmer, write little proofs in your head
26 points by soni
26 points by soni
Good stuff. Recommend https://cses.fi/problemset/ rather than leetcode to hone this set of skills.
In university in the early 80s we were formally taught about the work of Hoare and Dijkstra on pre-conditions, post-conditions, and weakest preconditions. It’s been enormously helpful over the years.
Also, if I have a complex loop then I find it very helpful to write it as a multiply-tail recursive function. This makes it much easier to prove correctness (in your head or not) because you ensure that each tail-call solves a slightly simpler problem than it started with. Modern compilers will turn it into GOTOs anyway, with the function arguments becoming loop variables.
As for constructing code, this seems to be almost totally unknown today, but “Jackson Structured Programming” is very useful for figuring out how to write any code that takes one or more input streams with internal structure and outputs another structured stream. This originated in COBOL batch processing, but it’s completely applicable to modern GUI programming or web programming, considering user actions as an input data stream.
You could also consider learning how to write formal proofs for your programs and then bring back that perspective back to semi-formal reasoning for everyday programming. There’s a very accessible book using Dafny called Program Proofs. You might come away with a newfound appreciation for how much easier a language like Rust makes it to prove functional correctness because for mutable data structures the main challenge is dealing with aliasing, even in a garbage collected language like Dafny where memory safety isn’t a concern. Dafny has a different solution to this (dynamic frames, frame conditions). [1]
Regarding assertion writing, I’ve noticed a lot of programmers (myself included) tend to stop short of writing proper verification conditions in assert form because checking such asserts (if it’s possible at all without a symbolic model checker) would degrade the asymptotic complexity of the surrounding code. For example, the key loop invariant for an array algorithm typically has one level of bounded quantifiers, which requires (at least) linear time to check at run-time. If the non-ghost code runs in constant time per iteration, you’re degrading the performance by at least a linear factor. This means it’s not a candidate for either assert or debug_assert macros (a reasonable expectation is that debug_assert should only degrade performance by a constant factor).
So, you probably need at least one more assert tier, e.g. logic_assert. That’s basically what verification-oriented languages do. You don’t have to go all the way and allow first-order logic (unbounded quantifiers) in logic_assert formulas; bounded quantifiers are usually sufficient (e.g. for the aforementioned loop invariants) and that makes it possible to do run-time checking, and you can still hook it up to a symbolic model checker. Or you could have bounded_assert and leave logic_assert for the full logic language.
[1] You could also take the alternative route of learning a proof assistant like Isabelle, Lean or Coq. But that’s going to focus your attention on issues that I think are ultimately less relevant if your goal is to apply what you learn to formal and semi-formal reasoning in everyday programming. The SMT-based verification languages like Dafny, WhyML and F* have their own serious trade-offs.
Guess I have been doing this for a while without putting a name to it! A little exercise I do, and try to show off when I pair with people, is “predict what will happen next, before I click the button” It’s usually in the context of debugging something, say, we made a change, reloaded our debugger, and are paused right before the moment of truth— debugger continue is “the button” here. It works in many places! Guess what state this database row will be in after we click the Transmogrify button in the UI, etc. If you’re right, it just feels good to be right lol, but if you’re wrong, you know your mental model is somehow wrong.
I get called a lot for using assertions in code, but I fight back and leave them.
Related: https://en.m.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence telling us that Proofs are (functional) Programs
Looking at Proof writing from that lens really helped me in my studies since I’ve been more familiar with functional programming and it’s made proof writing almost intuitive.
It’s hard to teach people about functional programming or even programming in general though so it doesn’t make proof writing easier for most
To be an even better programmer: put it in a comment.
This is the second most useful kind of comment you can write. The most useful kind is a description of why the naive method of doing something is wrong, or what parts of the spec were violated, so that you wrote the code the way you did.
It’s worth keeping an eye out for monotonicity, because you can usually use it to rule out wide swaths of possible outcomes. Another variation on this theme is immutability (which in a lot of ways is monotonicity’s cousin) - when you create an immutable object, that object cannot be modified.
On this topic, I’ve outlined some recipes in my blog post Monotonicity is a halfway point between mutability and immutability (2020), in case it helps anyone model their data monotonically.
A recursive data structure is a structure that contains a copy of itself (not necessarily an exact copy, but an instance of the same “type” of structure.) This copy can contain a copy, and so on; the process either goes on forever or terminates at a “base case.” A fractal, for instance, is recursive.
Hidden here is a more basic proof strategy: case analysis.
if (foo(x)) { ... } else if (bar(y)) { ... } and doing the case analysis to see what happens when e.g. foo(y).