Types correspond to propositions in formal logic, and programs satisfying that type are proofs of those theorems. This is called the Curry-Howard Correspondence.
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's been amazing learning about this. From "The Little Typer" book to Computerphile's videos on dependent (and homotopy, somewhat related?) type theory, to discovering Lean for interactive (math) proof construction, the history of it all dating back to Bertrand Russel trying to explain math from first principles, just wow. So lucky to live in a world where this is true.
No matter how many debug printfs you add to a program, they won't help you if you're editing a different copy than you are running. You will make this mistake and you will learn from it, but even reading this warning will not teach you, you must make the mistake yourself. If you are lucky, you'll lose only an hour. If not you'll lose a week.
When you train your mind to see the real world around you as lists of things that you can organize (and lists of lists, etc.—it's lists all the way down), more and more of your programming tasks become intuitive.
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.
A computer program is a theory of how to solve a problem, written by humans, in a format readable by machine. Most of the time, it will be humans doing the reading, the compiler only sees it sporadically. The run-time executable is a crystallization of the source code, freezing its structure for all time. (In the ideal case)
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.
Yeah, this is not precisely a "CS fact", but "you will git-blame a piece of shitty code and find a N-year old commit with your own name on it" is probably an unintuitive fact of programming that you only get to experience when you have a couple solid years under your belt.
Don't get stuck in code optimising it.
Typically the few ms you gain using a hash Vs an if/else is negligible to the read/write operation over a network or db that you may also have.
Optimise those instead with a cache and/or CQRS.
I've had quite a few junior devs ask me the above, so it's not always intuitive.
Looking up a small key in a table to get a value is easy.
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.
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.
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?)
So is Spark I guess. And that's a strawman and it says nothing about whether Scala is good or bad. Most people are taught OOP in class and they naturally move to a language like Java, which is familiar to them. From experience that's the number 1 people choose languages. This is also why people choose Python despite the fact that it becomes unwieldy for big projects. It's counter intuitive but despite Python not having static types, instead of a language with types like say F# they add all this extra mypy or other static analysis cruft on top of Python to make it into a chimera of a static typed language. Same with Java. Instead of coding in an expressive language people take an anemic language like Java and add complexity through extra language features like annotations with the consequence that the framework around it becomes more complex and something to learn, rather than the language itself.
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.
Which language is expressive in your opinion? I haven't used Scala but I think F# is a statistically typed language that stays flexible and is able to use types as an aid rather than a thing that adds complexity for its sake
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.
Well-known fact: Software architecture often follows team structure, or vice versa.
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.
Floating point math is not associative, (x+y)+z != x+(y+z). Most of the time the difference is small, but in some cases not (I.E. x = 1e30, y = -1e30 and z = 1, it is 1 in the former case, 0 in the latter).
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!
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.