Btw, the blog author, Andrej Bauer, is an amazing guy. I was really fascinated by some of his older blog publications (and I was only scratching the surface):

Btw, the blog author, Andrej Bauer, is an amazing guy. I was really fascinated by some of his older blog publications (and I was only scratching the surface): http://math.andrej.com/2007/09/28/seemingly-impossible-functional-programs/ http://math.andrej.com/2007/09/28/seemingly-impossible-funct... (by Martin Escardo, an article about a Haskell program doing exhaustive search over the “Cantor space” of infinite sequences) http://math.andrej.com/eff/ http://math.andrej.com/eff/ (Language Eff, a functional programming language based on algebraic effects and their handlers.) My understanding is that in this language all effects and evaluation order are explicit; effects and pure functions are easily and explicitly composable. Something like monads but more advanced. (My interpretation is probably wrong!) http://andrej.com/plzoo/ http://andrej.com/plzoo/ (The Programming Language Zoo). A number of mini languages which demonstrate various techniques in design and implementation of programming languages. (calculator, mini-ML, mini-Haskell, mini-Prolog, etc)