Talks that changed the way I think about programming

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.

Mike Monteiro: "F* you, pay me" - https://www.youtube.com/watch?v=jVkLVRt6c1U

Basically: When you try too hard to fit the real world into code, you end with OOP.

It has one great advantage: it is easy to translate real world into "computer".

but one great big distvantage: a computer is a computer, not real world, OOP translates to complexity (think "Architecture Astronauts", and spaghetti of pointers/references/virtual/inheritance) and things done in a way that harms performance (not a problem for smaller problems, but if your problem is not small...)

His idea is that you should instead fit the world into your DATA, not your code, think about what data your program needs from the real world (do you really need all tiny details for example?), what is your inputs and outputs, and THEN you code to make that work, you code around your data structures, file formats, etc... not the other way around.

Not exactly what you asked, but if you look at most subroutines in linear algebra libraries like LAPACK, they tend to have extra arguments so you can tell if your inputs are already transposed and/or conjugate in order to have more efficient memory access.