That might not sound particularly interesting, but here’s one of the ramifications: if you need to prove that your program follows some spec for eg avionics software or reactor control software, then one tack is to encode that protocol/spec in a type (usually an extremely expressive type system called a “dependent type” system) then you can prove a program correct to that spec and generate a program that is correct by construction.
This has been done. There’s a C compiler called CompCert where the optimization passes have been proven to not alter the meaning of the program. A tool called CSmith was used to fuzz gcc, clang, and CompCert and found dozens of bugs—but none in CompCert.
It even leads to understanding functional programming, mutability, referential passing, OOP.
You discover that many terrible programming analogies actually aren't terrible at all because you intuit their application better than with the analogy alone.
Why? Because CS is filled with practicable patterns that have real-world counterparts, and your brain synthesizes the complexities of the real world in myriad ways that just programming never could.
Since the audience is mostly human, write for them. Future you, who has forgotten the context, will likely be the largest fraction of that audience, be kind to them.
Looking up a big key can be done by looking up part of the key to get a second lookup table, in which the rest of the key is then looked up to get the value.
If the set of values is finite, the set of keys can be infinite by using a suitable graph of lookup tables. (this /!\ is the non-intuitive step)
If one can find a suitable compact set of functions, it's even possible to "look up" an infinite set of values: look up the right function for the key, then apply it to produce the corresponding value.
Real world challenges are not theorems.
Anyone who tries to fit it into narrow math concepts thinks he’s doing good, because math looks beautiful and intuitively beautiful == good.
But in reality (counter intuitive point) any formal and rigid system creates pain and suffering down the line when real programmers try apply those beautiful systems to real world _ugly_ problems.
One good example of such an overengineering is a Scala language.
Its features and elaborate typing system looks great on paper and artificial examples.
2. Users will do _anything_ you let them do
3. The customer almost never knows what they actually want
It feels the CAP theorem was more talked-about in the years of NoSQL frenzy. It is of course still highly relevant. Despite being widely known and discussed, I think it fits the "non-intuitive" description because most people really want systems to have all three (consistency, availability and partition tolerance).
2. Buridan’s Principle ( http://lamport.azurewebsites.net/pubs/buridan.pdf ) - A discrete decision based upon an input having a continuous range of values cannot be made within a bounded length of time.
This is more of a "philosophical" principle, but if you read the paper it does have practical implications.
Why? It happens because we organize both our software and our teams based on the amount of coordination needed to succeed.
Corollary: if the rates of change in your domains are accelerating and you start to accrue tech debt and cannot keep up, look for missing abstractions and the need to refactor both/either your software and/or your orgs. This tend to happen in glue roles (e.g. SRE, security), that sit at the crossroads of multiple efforts. Platform engineering is sometimes the solution for the org problems, but it requires all software components to present the same interface.
Modern compilers will reorder operations depending on a whole host of factors, and this means in general unless you really go out of your way, floating point math may not even be deterministic! I've seen this happen during certain optimization algorithms, completely different results on different machines even with the same random seed and confirmed same random sequence of numbers, it was because of the floating point reordering!
https://docs.oracle.com/cd/E19957-01/806-3568/ncg_goldberg.h...