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.
Working on the same code base for an extended time is great since there are plenty of humbling instances where you go "wtf" and git blame only to find your own name.
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.
just one of few such decisions in big projects I know of
https://cwiki.apache.org/confluence/display/FLINK/FLIP-265+D...
others I can't mention because not sure if I break NDA...
And if you work with scala on a big enough project - you'd know yourself the kind of pain I mean here.
Everything else in my comment is just a common sense (do you need any prove that the world is an "ugly" complex system that doesn't fit perfect math or functional programming picture?)
Im not proving anything.
Im just giving examples of problems.
If scala were that good - wed see more and more people migrating to it.
But it’s not the case - more and more teams prefer good old java (with all its own problems and legacy).
You call a statically typed scala language an expressive one? Lol :)
I agree with other points though.
But it only proves my original thesis that the world is ugly and there is no one solution that beautifully or magically solves it.
To be fair in comparison to java scala is not more shitty or more over engineered language.
The thing is that despite its “expressiveness” and mathematical beauty - it is still complex and ugly as shit when you use it in real world projects. Even if there are few exceptions like spark.
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.
the "eventual consistency" thing is what really threw me.
Weak Consistency may actually be a good thing? go figure...
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...