Climbing the Coq learning wall

So I am currently trying to learn Coq, this is a monstrous and Herculean task. It is one of those things where the learning curve is so steep as to deserve a climbing grade (I reckon about v6 for the intersection of the bouldering and PLT communities).

I have the Coq art book winging its way to me, but due to my remote location at the end of the earth (from the perspective of shipping companies, to everyone else I am in the capital of a developed country a days flight from Europe), it hasn't arrive nearly a month after ordering.

But, I Benjamin Pierce teaches a course on Coq and has made the lecture notes (which are all Coq scripts) available online (link is to 07's course schedule which has the whole course, as opposed to the current one):

http://www.seas.upenn.edu/~cis500/cis500-s09/index.html

This is an excellent tutorial for learning Coq from a PLT perspective and I highly recommend it - more so than any of the other Coq resources I've found online.

So, although tough, learning Coq is actually fun, and I hope will be useful. At the moment doing full proofs for a full calculus seems too daunting, but I can see that it is not as bad as some people make out, and hopefully once I have the hang of things will not be too hard. Also seems like a very interesting place to do research - there are so many things crying out to be studied.

Busy, busy

Sorry for no ETAPS report thus far. It will be coming soon. I have been very busy, jetting around, having very interesting discussions in London and LA and writing papers for ECOOP workshops. I visited Todd Millstein et al at UCLA and I blog a little about that too, all after easter.

For now I am back in NZ and going to visit Taupo tomorrow morning....

ETAPS 09

So, I've now moved to New Zealand, and in time there will be a post about all that, but right now I am back in the UK, in fact back in York, my childhood home - weirdly this is the longest I've spent in York for about 8 years and I'll have circumnavigated the globe to do it.

Anyway, ETAPS is at York university, which is very pretty - lots of grass and a lake and some ugly old buildings. It also, apparently, has the highest duck to student ratio in the UK. The downside of the venue is that most of us are staying in student halls, which although cheap(-ish) are not particularly luxurious. Pokey is a word that comes to mind - I at first mistook the bathroom for a cupboard. They also have a temporal-tardis-like effect - they appear older on the inside than on the outside!

Anyway, the first two days had interesting sounding talks, but were well outside my area of knowledge and so I gained little. Once ESOP started, however, there were many interesting talks and I will describe these in the following blog posts (over a few days).

ESOP paper

As I noted below (I think), my supervisor (Sophia) and I have had a paper accepted to ESOP 09 which is in march in York, England. The title is existential quantification for ownership variance and it can be downloaded here.

I'm moving to NZ tomorrow and looking forward to starting some proper research, as opposed to continuously correcting my thesis. Although not looking forward to the 27.5 hr flight so much.

Busy, busy,...

A quick update: on the academic front I have submitted my thesis and passed the viva with minor corrections, which I am working on now. Sophia and I have a paper accepted at ESOP 09 (link coming soon) on existential ownership for variance. Other than that I've been trying to learn Coq, which turns out to be very difficult. On the personal side, I got married and have been busy saying bye-bye to relatives and friends before we head off to NZ; talking of which, I got my visa yesterday, so now all I need to do is finish my thesis corrections and pack.

Things I don't like

Specifically, things I don't like in programming languages. When I design the world's perfect programming language, none of these things will be in it. I'm not going to justify any of these things, I am after all meant to be finishing my thesis.

arrays
overloading
pointers
inner classes
primitive types
raw types
private/protected/public annotations
Java-style reflection
non-reified generics
almost everything to do with concurrency
wildcards (the syntax, the underlying idea is nice)
packages
non-virtual inheritance
friend functions
\* *\ comments (rather then \\)

These are mainly OO/Java-ish things, I'm sure I could think of as many from other paradigms, but I'm a bit OO focused at the minute.

Some we just have to put up with because there is no neat, all round solution (eg primitive types). Others are not as good as they could be (reflection, concurrency support), and others just shouldn't exist (statics, arrays, most of the rest)

Feynman Quote

"Physics is like sex. Sure, it may give some practical results, but that's not why we do it."

Substitute "PLT" for "physics"...

Fun

Surprisingly, this is not going to be a post about functional programming, nor about the existential types calculus, Fun; but, about fun, as in "having fun" or something being fun to do. More specifically, programming.

OK, most people who know me will know that I hate programming. Well, that's not really true, I love programming, but I hate all the crap that goes with it. Writing neat, elegant code to achieve some task and see it work is more fun than most (but not all) things I can think of. However, testing, debugging, writing documentation, writing boiler plate code, maintaining code, all of these are about as much fun as a kick in the nuts.

I believe the fun aspect of programming is important, it motivates lots of people to write open source and free software and to code in their spare time "just for fun"! It pretty much explains why anyone would work in the games industry. Even in well paid development jobs, I think that tasks that are fun to do are given priority, done with more enthusiasm and concentration, and, therefore, done faster and with less mistakes.

So here's an idea for language design, how about making a language that maximises the fun in using it? It would maximise the time spent on fun things and try and make the not-fun things more fun, rather than more efficent or more safe or whatever other software-engineering-ey things are considered important nowadays.

Of course, you would need to find out precisely what was fun and why and how to put these ideas into a programming language, but maybe that will be fun to do itself.

How's that for a research project that will never get funded and will never happen?

Papers

I'm currently writing the background chapter of my thesis, and this involves a lot of re-reading of papers. Several times now I've thought "if only I had read this two years ago! This would have been so helpful, I could have avoid so many mistakes!" Of course, I had read the papers two years ago, and I thought at the time that I understood them (in the same way that I think I understand them (better) now). So, maybe, I should have put a lot more effort into properly understanding these papers when I first read them? Well, yes, I probably should, it would have saved me a lot of pain and effort. But, I can't help thinking that maybe I had to do all the work and suffer all the mistakes before I really could understand them. I like to think so, because then I don't feel so bad about wasting months on bad ideas that I could have avoided by spending a few days more on a paper.

p.s. I would particularly like to single out the two variations on the variant parametric types paper by Atsushi Igarashi and Mirko Viroli. It seems to be the paper that keeps on giving; I've read it at least five times now, each time in some detail, and yet everytime I seem to get more out of it!

Egypt

Currently I am in Egypt, to be precise I am in Dahab in the south Sinai. My mission is to write my thesis. I figured that it is a lot cheaper than London and there are a lot less distractions. So far I am doing quite well, I have written more than I think I would in London even though I have been busy moving into an apartment and settling in etc. Now I am ready to accelerate to never before seen levels of productivity! This is kind of dependent on the air con in my apartment getting fixed because otherwise it is too hot too sleep and far too hot to think, but, insha'allah, it should be fixed today.

My other reason for being here is that it is the freediving capital of the world. There is lovely warm, clear, and, most importantly, deep water 3 minutes from my apartment, loads of people to freedive with (most of whom are very good) and some great people to take some coaching from. I am pretty much on my pb from last year (41m) and it feels easy. I am taking it slowly, doing lots of dives to about 40m, and have some technique to learn, but I hope to be hitting 50m and more soon. So these are my goals for the summer - one complete thesis and 50m+. My schedule is pretty much work in the mornings, noon, and evenings and freedive in the afternoon. No late nights, no alcohol, no noxious London pollution; by the end of September I should either feel more healthy and alive than I have done in years, or a complete physical and mental wreck, we'll see...

Update, well I seem to be edging toward the physical wreck end of the spectrum, had a bit of boo-boo freediving and was spitting a little blood afterwards. Apparently not too much to worry about, but need a few days rest and to take it easy for a week. That will teach me for being so optimistic! On the bright side it means I have even more time to write my thesis, so I am plowing ahead with the background chapter!