Hacker News Reader

> These talks are a little skewed to the game/high performance programming side of the art, but still very interesting in general.

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.

> 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

Could you point to some sources?

This is the paper people usually use to explain some of the performance benefits you could reap, besides the talk about row vs column based performance:

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).

+1

> 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.

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.

For some, there might be some valuables on these interviews:

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 "hole-driven" development style originated in dependently typed languages such as Agda and Idris, which I imagine Matthew's video was inspired by. So if you want to experience it right now, go learn Agda and use agda-mode in emacs. (Probably something similar exists for Idris. I don't know whether Coq has a notion of "holes".)

idris-mode for Emacs does similar tricks ( https://github.com/idris-hackers/idris-mode ) and I've heard it's very nice.

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

> The programming style demonstrated in this video is a real mind bender