I get the chance to interact with a pretty wide range of software engineers, the thing that constantly blows people's minds is how caches work and the fact that there's 10-50x performance waiting for you if know about it(and have the time to exploit it).
It's almost like they don't teach it in school or something, I agree there's a lot of gamedev/perf stuff but that lines up with my experience of things that change the way people approach programming.
Could you point to some sources?
https://www.akkadia.org/drepper/cpumemory.pdf
Note that I wouldn't really recommend it unless you're really going to do low level programming for high performance. It's super long, explains all the details, if you've got a basic CS college education you should know most of it already anyway.
If you're just a web developer this won't actually help you as most of this improvements have already been done in the parts that matter (i.e. your database, your operating system, your interpreter and perhaps your application server).
As mentioned below, this can be used in languages like Agda and Idris; they also give you proof search, which tries to automatically fill in the holes from available definitions. This works well for 'proof objects' (the name given to values which only exist to satisfy the type checker), but requires caution for values with 'computational content' (those values which can effect the resulting computation).
Pretty much all Haskell code (except the really wacky astronautical stuff) has computational content, so there are fewer "obvious" obligations to fill in than would appear in a proof (in fact, due to laziness and lack of totality, we can safely use 'undefined' for all proof objects, since they'll never be pattern-matched!).
For example, if our function needs to return a list (e.g. if we're writing a function like map, filter, iterate, replicate, cycle, etc.), a proof search will immediately give us the empty list '[]', which is correctly typed but probably wrong.
For Haskell, tools like djinn can get you a little hole-filling automation, and I think that Emacs modes like ghc-mod and intero support calling out to djinn (I can't test this, as I can't get either to work on NixOS :( ).
For a little more work, you could write properties for QuickCheck (/SmallCheck/LazySmallCheck/etc.) to constrain the behaviour, which would allow trivial solutions like the empty list to be ruled out automatically. If you're a TDD disciple, then you already wrote these properties, so this part would actually be free (as long as the automation tooling exists).
At that point you're basically doing inductive functional programming, so tools like IGOR2 or MagicHaskeller might be useful to plug in as well.
https://www.youtube.com/watch?v=QVpSIdWE0do&list=PLEMXAbCVnm...
Again, it's game dev oriented, but there are good general advice as well, here and there.
Mike Acton is on there too. Jonathan Blow, Ron Gilbert, etc.
In general, I think more programmers should be concerned with learning how things work at a deeper level than the API for whatever web framework they are using. Web applications are god-awfully slow, it's like the programmers behind them just don't give a shit about performance, at all. It's not that much better on the desktop side either.
The Idris REPL itself can do hole-based programming too, which can then be dumped out to a file (:m to list holes, :p to prove a hole, :a to write proofs to disk) http://docs.idris-lang.org/en/latest/reference/repl.html
You might also be interested in:
https://hackage.haskell.org/package/djinn
Djinn writes the code for you. Cut out the middle-man. (Don't show your boss.)
Since this has become such a nice thread some additions I'd add:
* Sandi Metz going through the Gilded Rose or "All the small things"
https://www.youtube.com/watch?v=8bZh5LMaSmE
I already subscribed to her programming style and the general Ruby TDD/BDD movement, but this talk captures all the important values in a single example. I think it made my programming style no longer based on vague things like experience or intuition, but just on concrete merit shown in this talk.
* Matthew Brecknell demonstrating Hole Driven Development
https://www.youtube.com/watch?v=52VsgyexS8Q
The programming style demonstrated in this video is a real mind bender. I think most Haskell programmers use a weaker version of this, Matthew takes it to the extreme. I didn't adapt this style, I don't think it's practical, but it's the sort of thing that some person someday will incorporate in some more comfortable way in a new language or platform as a revolutionary feature.