I’m enjoying reading this. The language is very accessible and the concepts are introduced at the right pace for me.
One thought that has struck me when learning about types/type checking is that we were taught to do this in physics classes. We called it checking units. It was a primary sanity check to any formula we had derived if the units, after the divisions, multiplications and additions required in the formula, came out consistent. If they didn’t you were guaranteed to be wrong. If they were consistent, well you did more sanity checks.
Yes - when I write code in languages with rich type systems, I write the types first, and I absolutely think of it as analogous to the physical unit thing. If my expression doesn’t do what I thought it did, the compiler will almost always tell me so.
I once saw Knuth reverse-engineer a Mayan algorithm, and note that “it blithely adds a length to an area” but still gets the right answer. You can definitely make physics equations work without units; it just places a higher burden on the person coming up with them!
“it blithely adds a length to an area” but still gets the right answer
I’d be curious to see that!
I believe his write-up was collected in a long-ish book collecting many of his papers, and I believe it was called something like “Knuth’s Fun and Games”. I can’t easily check because it’s not the only collection book he’s published, and my library is in boxes waiting to be unpacked someday…