Hacker News new | comments | show | ask | jobs | submit login

If we attempt to apply Tao’s three stages -- pre-rigorous, rigorous, and post-rigorous -- to programming, something interesting happens: we find that the programming world is mostly stuck at the pre-rigorous stage because there is no widely accepted theory to guide practitioners to later stages. Yes, computer science has an accepted theoretical foundation, but computer science is not programming.

In programming, the closest I’ve seen to a widely practiced theory has come out of the Haskell community. There, you can see the beginnings of a theory in which programs are constructed out of formal building blocks like monoids and functors and where appeals to category theory and monad laws guide design decisions.

It’s a start.

This is the most clear explanation for what I enjoy about the Haskell community I've ever read. I am utterly addicted to Conor McBride's [1] work as well since he's doing the incredible thing of answering semi-practical questions with deep dependent typing theory. I also think Gabriel Gonzalez's [2] writing has the right ideas as he tries to explain the feeling and heuristic of using categorical and functorial design while also writing a very beautiful library [3].

I also really can't get away without mentioning Edward Kmett[4], Conal Elliott[5], and Edward Z. Yang[6] for writing both blog posts and code expanding on the practical advantages of theoretical methods.

[1] https://personal.cis.strath.ac.uk/conor.mcbride/ further work available extensively at StackOverflow, user Pigworker (http://stackoverflow.com/users/828361/pigworker) and you should definitely attempt to read Kleisli Arrows of Outrageous Fortune if you're interested in some dependently typed madness.

[2] http://www.haskellforall.com/ and especially http://www.haskellforall.com/2012/09/the-functor-design-patt...

[3] http://hackage.haskell.org/package/pipes-2.5.0

[4] http://comonad.com/reader/

[5] http://conal.net/

[6] http://ezyang.com/

Dan Doel [1], who works with Edward Kmett, gets it too.

And there's the inimitable Luke Palmer [2], whose blog contains nuggets of gold for those who care to dig through the archives.

[1] http://www.reddit.com/user/doliorules

[2] http://lukepalmer.wordpress.com/tag/haskell/

Having done a substantial amount of both math and programming, I feel like I can say that a start is all you will get, ever.

Most of the intuitions of programming are not provable and will not become provable, ever. I think I can back that up using the properties of the arithmetical hierarchy from Yu I. Manin.

Guidelines | FAQ | Support | API | Security | Lists | Bookmarklet | Legal | Apply to YC | Contact