Recent searches
Search options
Never thought about it this way before.
"We teach algorithms so that students learn to think about invariants and properties when writing code."
From "Fantastic Learning Resources" by matklad: https://matklad.github.io/2023/08/06/fantastic-learning-resources.html
@dubroy i've given so many different answers to the question "how often do you actually use the stuff you learned in your cs degree?" (alternatively: "how many years does it take before you actually use...")
this is so much better an answer than any i've ever provided.
@dubroy I don't disagree but that fact that this comes across as revelatory is a sad indictment of how we often teach in our field
@dubroy This observation will be unsurprising to the generations of Cornell students who took introductory programming courses from David Gries :-)
@jacobsa @dubroy absolutely. I routinely teach programming in terms of informal proofs. every now and then I go read part of a book about invariant-based programming, there are a few of these. also every now and then I get to teach a course that centers this kind of reasoning. but most people make it through our program without major exposure to this
@regehr @jacobsa @dubroy Would be interesting to see a list of those invariant based programming books. (Ever since I've seen the 'theorems for free' paper I focus more on types and data structures than implementation).
One successful example of thinking about invariants/properties was the way backtracking was taught in high-school. There was a template with separate functions that you had to fill in with the properties specific to the problem, and a high-level , almost boilerplate, code for the actual algorithm. This was a lot more verbose than just coding it all directly in a single function, but was very useful for learning. In fact even at competitions there were some who started by typing out "the backtracking template" to save time, even before they got to see what the problem was. So in case they run out of time to implement a more efficient solution they'd at least score a few points on the smaller test cases, as it was relatively easy to fill in the template with the properties, and thinking about those properties was a necessary step to find a more efficient solution anyway.
Nowadays I tend to take this a step further and try to use the type system/abstraction to enforce invariants (at compile time if possible). Far too often I've seen code that claims to be OOP, but is so only in its syntax, and doesn't actually take advantage of abstraction and exposes all the internals with getters and setters that might destroy any invariant. Whereas when used properly, OOP (or abstract types in modules ), could ensure correct by construction values, that can only be modified by update functions that themselves guarantee to preserve invariants (ideally also immutable, which works nicely in a functional language).
here's a list of links I had sitting around:
https://hal.science/hal-00477903/document
https://www.cs.tufts.edu/~nr/cs257/archive/robert-paige/invariants.pdf
http://www0.cs.ucl.ac.uk/staff/p.ohearn/papers/Marktoberdorf11LectureNotes.pdf
https://www.danielzingaro.com/invariants.php
https://people.cs.ksu.edu/~dwyer/papers/ICSE02.pdf
of course this is incomplete, for example we would want to include _A Discipline of Programming_
@edwintorok @regehr @dubroy This is probably a well-known idea and I’m embarrassed to admit I only fully internalized recently, but: it clicked for me when I was told the point of an _object_, in the sense of a class in C++, is to defend internal invariants across its members. As opposed to a “PoD” product type like an aggregate in C++, which is just a composite value and cannot usefully have invariants across fields.
Such a simple idea; I wish it had been taught to me like that originally.
@edwintorok @regehr @dubroy And then I guess the inverse was very useful to me too: if it doesn’t need invariants *across* fields, then a plain aggregate struct is fine. Don’t spend all your time writing annoying boilerplate accessors (and calls to them) if there are no invariants to maintain; it’s a total waste.
@dubroy Oh huhhh
That is really cool! I will definitely read some more on this topic!
I suspect I would find this more enlightening if I understood what he means by "invariants."
@dubroy Yeah, I always considered learning those things to mostly to confront our brains with complex structures and keep remembering some of the strategies that are helpful. Computer Science was basically an "here's as much complicated and complex stuff that makes your brain explode, and if you get through that, real life stuff will be easier".