Yeah, focusing on the highest value is great advice. Nice list! Regarding FP, I think it's cool that there's so much activity and open source stuff going on, a

Yeah, focusing on the highest value is great advice. Nice list! Regarding FP, I think it's cool that there's so much activity and open source stuff going on, and from the community perspective it's a fresh angle for talking about correctness and reasoning and stuff. Xmonad was a great community project for "teaching the virtues." Being a hacker's window manager, it was all about extensibility and configuration, kind of like this coral reef of experimentation. John Hughes used it as a big example when he gave talks on "real world" FP. The architecture is basically a pure core of compositional/algebraic/combinatoric stuff, with around 100% test coverage including lots of QuickCheck properties... surrounded by an interpreter layer that realizes this stuff into X11 commands. So I'm really interested (not scholarly or academically or even professionally, just hobbyishly) in being able to express domains with actual logic. And since my interest's trajectory starts at Haskell and goes through Agda, I'm fascinated by the ability to unify proofs and programs (due to the Curry-Howard equivalence of typed lambda programs and constructive logic proofs). I'm kind of waiting for more of that stuff to start growing in the open source / startup / GitHub / HN ecosystem. It ought to be very fruitful. With these new dependent type languages, proving becomes like hacking—you don't need to start as an academic logician, and you can bypass philosophical arguments about the definition of truth, because you just want to engineer a type-checking proof. So I think people could have fun with it. But there's a lot of alien notation and scary stuff... Let me nerd out for a while since you seem interested, and I wanna spread the word about some things. QuickCheck of course is a tool originally for Haskell that lets you very easily verify equational properties using type-directed random value generation. It's used in tons of real Haskell projects and it's super awesome. Recently I was writing a thing to synchronize Reddit comment state with a Git repository, and I used QuickCheck to verify that some JSON conversion things were isomorphic—this is a typical case where QuickCheck can instantly find tricky bugs and you barely have to write anything: quickCheck (\x -> parse (render x) == x) gives you a powerful test suite, even if the types have lots of nesting. Then, a later project that's not as well known is QuickSpec. http://www.cse.chalmers.se/~nicsma/papers/quickspec.pdf http://www.cse.chalmers.se/~nicsma/papers/quickspec.pdf https://github.com/nick8325/quickspec https://github.com/nick8325/quickspec (pretty good README) It's kind of the inverse of QuickCheck: you would tell it to search for true equations involving parse and render, and it would discover the isomorphic property. It does limited exhaustive search on application trees, and randomized testing for verifying equations. So it can be a great starting point for reasoning about your modules, if they're written in a way that makes them amenable to algebraic reasoning. And then the next step is HipSpec. http://www.cse.chalmers.se/~jomoa/papers/hipspec-atx.pdf http://www.cse.chalmers.se/~jomoa/papers/hipspec-atx.pdf https://github.com/danr/hipspec https://github.com/danr/hipspec It takes equations about Haskell functions, and then uses off-the-shelf automated theorem provers, combined with automatic lemmas from QuickSpec, to generate formal proofs automatically. All this is made to work on actual Haskell code, and I think it points out a really cool path for getting hackers to bother with proofs and equations. What I haven't seen so much yet, and this is one of my biggest curiosities / vague ambitions, is how to take different diverse domain models and extract an algebraic core. Xmonad did it for window managing, which is super nice. I'd love to see more of that in different domains. As I see it, that's what's going to make more people see a tangible value in otherwise abstract seeming stuff like equational reasoning. This is already long enough, but a quick pointer to another eccentric interest I have, due to my brother who's great at finding value in seemingly obscure realms, and sticking with it even though people say he's crazy... Interactive fiction is all about modelling objects and situations in a way that's comprehensible to humans, especially if you look at e.g. Inform 7, which uses English grammar as the basis for its declaration language, and has a very nice declarative modelling paradigm, quite novel stuff. So that in itself is awesome, and I'd love to see some non-fiction programs written in Inform 7. It compiles to a virtual machine that as far as I know is decently fast and has I/O capabilities. Then there's work by Chris Martens, which has been linked on HN at some point, on using linear logic as the basis for interactive fiction and general game prototyping. > My thesis project is a programming language for the design of interactive narratives and game mechanics. The language is based on forward-chaining linear logic programming, a way of declaratively describing state change. This methodology makes it feasible to encode generative rules that create procedural content for interactive simulations that give rise to emergent narratives. > The language semantics' basis in proof theory enables a structural understanding of these narratives, making it possible to analyze them for concurrent behavior among multiple agents. On a larger timescale, I imagine growing the technology underlying this language into a high-level sketching tool for game designers, usable for rapid prototyping and iteration. http://www.cs.cmu.edu/~cmartens/ http://www.cs.cmu.edu/~cmartens/ So my crystal ball shows some really fascinating and awesome stuff coming out of that whole tradition in the somewhat near future... Um... let's see if I'm even allowed to post this long comment...