"My story roughly speaking is that I came out of Chalmers all gung ho about dependent types and probably correct functional programming, and now I work on a JavaScript startup with not even many unit tests (which is partly my fault)."
I tell people to focus on just what delivers the most value. I came up with a list of the few things that are empirically proven to benefit software quality:
So, for Javascript, you might do code reviews, use any static analyzers you know, decompose into functional style, have some interface checks encoding assumptions, and so on. Simple techniques that take little time, save you much time, and boost quality greatly. Plus, recall that you can do FP in many languages by subset and style. ;)
Note: This doesn't even count my old strategy of making a safe, macro-enabled 4GL that compiles to a target 3GL. You can code up shit in ML or Dependent language with constructs that can map 1-to-1 to JavaScript. Then, your tool produces Javascript from whatever you really code in. You deliver that w/out mentioning other tool. Best of both worlds.
I caught that: "I meant to say provably"
Not that: "but the autocorrect typo is illuminating" Lol nice catch. The autocorrect might have corrected an entire field's thinking rather than one person's spelling. You should contact the authors about the discovery of AI in their software. ;)
"Xmonad architecture"
I wasn't aware of it and I don't do functional programming yet. I'll have to add it to my list of things to check out.
Regarding provably-correct FP, what was your background, tools or projects? I might learn something or have something your interested in as I collect work in high assurance field. Have quite a few on that topic including some explorations but lack specialist expertise to really evaluate it.
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.
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.
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.
I tell people to focus on just what delivers the most value. I came up with a list of the few things that are empirically proven to benefit software quality:
http://pastebin.com/xZ6m4T8Z
So, for Javascript, you might do code reviews, use any static analyzers you know, decompose into functional style, have some interface checks encoding assumptions, and so on. Simple techniques that take little time, save you much time, and boost quality greatly. Plus, recall that you can do FP in many languages by subset and style. ;)
Note: This doesn't even count my old strategy of making a safe, macro-enabled 4GL that compiles to a target 3GL. You can code up shit in ML or Dependent language with constructs that can map 1-to-1 to JavaScript. Then, your tool produces Javascript from whatever you really code in. You deliver that w/out mentioning other tool. Best of both worlds.
I caught that: "I meant to say provably"
Not that: "but the autocorrect typo is illuminating" Lol nice catch. The autocorrect might have corrected an entire field's thinking rather than one person's spelling. You should contact the authors about the discovery of AI in their software. ;)
"Xmonad architecture"
I wasn't aware of it and I don't do functional programming yet. I'll have to add it to my list of things to check out.
Regarding provably-correct FP, what was your background, tools or projects? I might learn something or have something your interested in as I collect work in high assurance field. Have quite a few on that topic including some explorations but lack specialist expertise to really evaluate it.