Satori is pretty weird

I achieved satori, and it's kind of fucked up. Everything is a programming problem. Look at a piece of toast and you'll see an endomorphism on the domain of bread. Look at a chair and you'll see a recursive descent parser. Look at a dog taking a shit and you'll see a novel set of inductive laws for reasoning about infix notation.

I mean, I did swimmingly at the program I was working on, but it would be nice to brush my teeth without having to check my floss for null.

>>19
He links to a paper by a homotopy type thoery guy, so assumedly he does.

>>17
Your second link was a tongue in cheek response by master Haskell programmer Conal Eliott amidst discussions on what makes a language purely functional. It's not a serious argument, just humorous and playful nudge at some colleagues to stop wasting their time.

However I will add that the homotopy type theory is a brand new take on all of mathematics coming from three or four people who were``purely functional'' (LOL) Haskell, and Agda etc. programmers, not really mathematicians; the foundational book of the field is hosted on github.

Outside of the Haskell community as it appears on reddit, hacker news, and the blogs of the people who discovered this new take on all of mathematics I don't think the world acknowledges their existence, and I certainly don't think any real mathematicians care too much about what they do.

I'll let you judge for yourself whether to take them any more seriously than real programmers (i.e. Common Lisp programmers) take the functional programming trendroids.

As a social commentary, compare e.g. Gerald J Sussman, a real mathematician and master programmer, and his research interests to the homotopy and Haskell people. The latter are obsessed with restricting your programs to match some sick paedophilic notion of ``purity'' in order to be able to analyze them, the former is obsessed with crafting useful programs to analyze the real world.

Alas