Jason (jcreed) wrote,
Jason
jcreed

In the shower this morning it occurred to me to list the languages (I'm being fairly inclusive here) I've touched in the last year in the course of doing work:

C++, C, C#, Java
SML, Caml, Scheme, "fuzz" (the last being the little functional language that we made)
Twelf, Agda
Perl, Javascript, Shell scripts

The remarkable thing is how unremarkable this is, I think; we all have to use various tools to get our work done.

Agda I've only been playing with in the evenings since ICFP, working on this little representational experiment with Dan Licata. Already I'm feeling very strongly that, e.g., Adam Chlipala's frequent advocacy of more automation in proof assistants is a valid point. Even if it's foolhardy to hope for sophisticated automated program synthesis (and even then it's probably not --- we are making pretty good progress there) there are so many little gaps that are essentially about constraint solving problems that are more often uniquely solvable than not. Twelf knows how to split cases on a type, but twelf-emacs-mode doesn't know how to textually insert a bunch of boilerplate and sheds for me --- but agda-emacs-mode does, and it makes me awfully happy.

This sort of benign, simple automation (well, to the extent that doing a bunch of higher-order unification in the background is simple...) really is playing the same role that type-checking per se is playing in the wider world of programming. One might say that the more macho hardcore programmer should be able to slice and dice all the invariants in their head without being a wimp and letting the compiler help them. But fuck that; me plus type inference is a more efficient system than me alone. Just like me plus a pocket calculator is a more efficient system than me alone, even though I might not be a mental-arithmetic whiz as a consequence. I can focus on the interesting difficulties and ignore the mechanically-solvable difficulties.
Tags: math, programming, tools
Subscribe
  • Post a new comment

    Error

    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded 

  • 8 comments