I started a blog in 2007 with great excitement, but then it languished. Now, after a year and a half of inactivity, I have migrated it to WordPress and plan to continue writing!
One of the key goals I have here is to provide an outlet for the many half-finished programming projects I have sitting around. Most of them have reached the point of being marginally useful, but each one has some technical problem that I have wanted to resolve before letting it loose.
This is silly. If I’m going to make something open-source in the end, I might as well do it from the beginning. Maybe the rough beginnings won’t be useful to many people, but they won’t hurt anyone. After all, one open source mantra is “release early, release often”.
So, today I uploaded two small and incomplete, but potentially useful, projects to GitHub. Both are Haskell programming tools for OS X.
The first is a QuickLook plugin for syntax highlighting of Haskell source files. It basically works, but does a few silly things like hardcoding the search path for HsColour. It’s a fairly reasonable search path, though, and likely to work on many machines. So, here it is:
Another little project I wrote up about a year ago, and then put on the back burner, is a library for interacting with DTrace from Haskell programs. It’s a tiny library, and probably doesn’t fit the standard DTrace philosophy that tracing should have no overhead when disabled, but it could be useful as-is. And the performance issues are fixable. So here it is:
A few weeks ago, Leslie Hawthorne from Google interviewed some people who’ve done Summer of Code projects for Mono over the last few years, including myself, Alan McGovern, and Michael Hutchinson. It just went up on the Google Summer of Code blog, here.
In the last two years or so, I’ve written far too many programming language soundness proofs. In many ways, the proofs have been fun, but I never feel confident that they’re correct. I can go over the obviously tricky bits several times, and convince myself that those particular arguments hold. I can ask other people to proofread them, and often catch mistakes that way. But, after a certain point, poring over dozens of pages of induction proofs just makes my eyes glaze over.
Computers have much more patience, and I want them to check my proofs for me. To this end, I’ve tried a few proof assistants. I’ve actually finished non-trivial proofs in both Coq and Isabelle, so I thought I’d give a brief description of my experience with each. While I have some sense of the pros and cons of both systems, I’m not an expert in either, so forgive me if I get some of the details wrong.
I started with Coq, at the end of 2005. I chose it first partly because of its strong showing in the POPLmark Challenge, since I was planning on using it to prove things about programming languages. My experience with it was a mix of addiction and frustration. Xavier Leroy (I believe, though perhaps I’m making it up) commented that pushing theorems through Coq was like playing a video game, and I agree. You can’t put it down, but it eats up more time than you’d like to admit.
I found that writing down the structure of a formal system in Coq was quite easy. In fact, it tends to be easier than writing up the rules in LaTeX, an inevitable step for anything that will be published. I also found that just encoding the system, without any attendant theorem proving, was valuable in itself. Coq type-checks the definitions, and performs some other well-formedness checks, which is much more than you can expect from a typesetting program. In fact, Coq’s basic checking uncovered the most serious bug I’ve found in any language I’ve been involved in developing.
I didn’t find writing actual proofs in Coq to be quite as easy. Once I got going, walking through a maze of proof states was sort of fun, but kind of distracting from the high-level goal of actually proving a theorem. And the resulting proofs tended to be far from readable. I shouldn’t overstate this point — some of the Coq proofs I’ve seen are actually fairly readable and to the point, but it’s definitely easy to wind up with a long stream of proof tactics that mean almost nothing without the context of the associated proof states.
For the next year I didn’t do much with proof assistants. Then, in early 2007, I started to pick up Isabelle, partly inspired by Jeremy Siek and Walid Taha’s proof of the soundness of their gradual typing system. At first, I didn’t like Isabelle’s syntax as much as Coq’s, and didn’t quite understand how the structured proof language worked. So, for a while, I had no reason to prefer it over Coq.
Then I wrote my first structured, forward proof in Isar. I fell in love. The proof was as readable as the LaTeX version I had already written, if not more so. It was also easier to write, and machine-checked! Granted, it was easier to write partly because I already knew exactly how the proof went, and it was not a very complex proof at that. Nevertheless, I have reached the conclusion that I never want to write an induction over type rules by hand again. Writing it in a formal language with mechanical verification is just too seductive to pass up.
Although I fell for proof assistants most completely when I discovered Isabelle, I don’t want to sell Coq too short. It has a number of nice advantages, which may tip the scale the other way in different circumstances. For instance, you can write proof tactics (essentially, miniature automatic theorem provers) in Coq using a special tactic language without recompiling anything. Writing tactics in Isabelle requires editing ML code and recompiling the system. In addition, Coq can extract executable programs (in OCaml, Haskell, and Scheme) from function definitions used in your proofs, ensuring that the resulting code satisfies whatever properties you’ve proved about it. As far as I know, Isabelle doesn’t do this.
For now, I’m using Isabelle because of its structured proof language (Isar), extensive LaTeX support, and large libraries. Those three features are almost indispensible. Essentially, I think that Isabelle has a leg up at the moment because it has a larger user community (it seems), and has been around longer, so it has had more time to develop nice trimmings.
Coq, on the other hand, is a younger system, but potentially more powerful. I believe that a structured proof language for Coq is in the works, and adding better LaTeX support seems like no huge problem. And the libraries of Coq proofs and tactics seem to be growing. So I may lean back toward Coq at some point.
Regardless of the actual system, I think the time for machine-checked proofs is here. I have found that the process of formalizing a proof in Isabelle hardly takes more time than it would to work out the proof on paper and then type it up (in LaTeX, for instance), and it sometimes takes considerably less effort, since the computer frees you from keeping all the fiddly details in mind at once.
Give it a try.
I have a love-hate relationship with TeX/LaTeX, and I know I’m not alone. It produces beautiful documents (most of the time), but has a baroque, hard-to-type, error-prone input syntax and a first-order macro language. LaTeX style files are often an especially unreadable mess.
What could improve the situation? Ideally, I’d like to see a totally new input language attached to the TeX rendering engine, or perhaps a modified version of it. This new input language should have at least the following properties:
- Plain text should be almost valid input, as in TeX.
- Markup should be easy to type! Less need for the shift key and the symbols on top of the number keys. Square brackets, single quotes, periods, commas, slashes, and semicolons are good. Curly brackets, dollar signs, percent signs, and ampersands are less good.
- Markup should be made up essentially of expressions in a functional language.
- Expressions should be statically typed, to hopefully facilitate better error messages.
- Layout algorithms should be improved to allow better integration of graphics and text, so that it can be more usable for the style of layout advocated by Edward Tufte.
- Unicode input should be allowed (as, of course, it is in some variants of TeX).
- It should make use of the capabilities of modern document standards (i.e., use PDF or Mars as a primary output language, with Type1 or OTF fonts). Things like (X)HTML, or other XML encodings, might also be good.
I’ve had several conversations lately with fellow students about the possibility of creating such a language, and at least one person agrees with me that some sort of DSEL built on top of Haskell might be a nice choice (see here).
Of course, it’s much easier to come up with a simple list of features than to actually design a full language. Knuth put a lot of work into designing TeX, and while many things are awkward, most things are possible. It would be nice to have a new syntax that is both more expressive and more concise, and that’s not a trivial task.
Expect more writing on here at some point once I’ve given the matter more thought.