Experimenting with CompCert

A few weeks ago I experimented with CompCert, a C compiler from INRIA, written largely in Coq, with chunks in OCaml; this allows the Coq parts of CompCert to be formally verified (see below for more on this).

Now I have no need of a guarantee that my compiler is bug-free, but to the extent that translation my code into the subset of C supported by CompCert reduces the bugcount rather than increases it, it’s a win. I’m basically using compcert as a lint tool, but it’s fun and instructive anyway. The real-world scenario which makes any of this interesting is therefore if you have a C codebase and suspect a bug in your compiler and want to know how hard it would be to maintain that codebase such that it compiled with a compiler believed to be bug free.

For many years I have maintained a codebase of 40K lines of fairly odd C, that implements a computer game I used to run in the 1990s, and which predates modern conveniences that might have been used, such as sqlite, pcre, libevent, reliable IP stacks on NeXTSTEP, ANSI C, free C++ compilers, free Erlang, etc, etc. The code is also unusual in shunning the use of struct, malloc and pointer arithmetic. For almost the last twenty years I’ve kept it up-to-date with the C toolchains on a number of OSes, as a way of keeping an eye on what the cool kids are breaking.


Firstly, the codebase needs to be able to cope with multiple compilers; gcc and LLVM’s clang are close to drop-in replacements for each other from the perspective of the Makefile. Not so, CompCert: -Wall -Werror are not accepted as options by CompCert, as they’re effectively on by default. CompCert isn’t going to want to know about any code that doesn’t pass gcc -Wall -Werror, but there are a few things LLVM thinks it’s Ok to warn you about that CompCert is cool with, which feels like LLVM is wasting my time. Getting the build system and revision control happy about parameterisable compiler options has to happen first.

I was forced to do change all the remaining instances of conflation of integer widths. Anyone who’s done arithmetic in OCaml will recognised this as one of the house microfascisms of INRIA, but it’s a deep issue: a lot of corner cases depend on your installation of the header files and libraries and so on. In my case, function prototypes are culled into a .h file automatically with cproto, which by default changes the width of integers in K&R-style C functions:

void my_function(i)
short i

is output as

void my_function(int i);

which gcc and LLVM tolerate, but CompCert doesn’t. There were a couple of other legitimate “Well Don’t Do That Then” moments that I won’t tax you with. Effectively one’s forced to get all the prototypes and headers and includes exactly right. This showed up a bug: a variable which was supposed to be declared extern wasn’t, and was separately allocated from the global it was supposed to represent.

The more formal treatment of integer widths also meant fixing a lot of sprintf format strings.

The next thing I had to fix was the idiom

    char *messages[] = { "...", "...", "...", NULL };
    int x = sizeof(messages) / ...;

CompCert insists on the length of messsages[] being explicitly specified, which means this technique isn’t allowed.

The harder stuff was signal() and stdarg; basically, CompCert supports an anaemic subset of C, and doesn’t allow stdargs, though it provides the sprintf() clique of functions. Since wrapping sprintf() is about the only thing varargs is used for in C, this turns out not to be a problem, but I originally bet that parts of the codebase were outside the CompCert C dialect and would need to be shunted into libraries.

My own adventure in CompCert land basically amounted to learning new stylistic restrictions in C. Reading around what people have been doing with CompCert I came across a few interesting articles and from this chap I learnt about concolic testing which is another technique I have no use for but am glad to have spent time learning about.

If you could bear reading this far, you should follow me on Twitter:

An independent Scotland will be outside the European Union

If the people of Scotland vote to leave the United Kingdom this week, customs checks along the new border are practically unavoidable. Alex Salmond claims that Scotland will continue to be part of the EU. He’s bluffing, and without membership of Europe’s Customs Union, his newly independent country will no longer be able to export goods to England tariff-free: anything crossing the border must be examined and taxed, and a cut sent off to Brussels.

It’s perfectly possible for Scotland to rejoin the EU after 2016, and the difficulty of doing so is being exaggerated by unionists, but automatic membership is legally impossible. The members of the European Union are states, not peoples or territories, and to gain membership a state must be approved by the governments of all the other EU member states.

Except in France.

Under Article 88-5 of the French constitution, the French Government no longer has the power to approve new EU member states by itself. The political elite there is so distrusted that new states must be approved by the people in a referendum, or by a supermajority in Parliament. Has Mr Salmond made a secret deal with the French people, or perhaps with the rightwingers and nationalists of the French opposition, or is he just winging it again? The French are not going to ignore their own constitution to help the SNP, as letting the French political class admit new countries to the EU means letting Turkey into the EU, and that is about as popular in France as cutting agricultural subsidies, so somehow the politicians or the people need to be bargained with.

Even if Salmond said he hadn’t made a secret deal with any foreign rightwinger other than Rupert Murdoch, we should not believe him: his administration spent thousands of pounds of taxpayer’s money trying to prevent the disclosure of legal advice on Scotland’s EU membership when in fact this advice didn’t exist in the first place. Would you believe non-existent advice from this man?

For an indpendent Scotland to rejoin the EU, it needs to conclude a treaty with the existing member states, including the rump UK. This can’t be done while Scotland is still part of the UK (particularly from the perspective of the French constitutional requirements). This means months or years of disrupted cross-border trade and customs checks along the Tweed, at Euston Station and so on while the other countries sign up.

Much has been made of the potential attitude of governments in Spain, Cyprus, Greece and other places with sensitivities about secessionism. Particularly troublesome are countries such as Spain and Cyprus which have territorial claims against the UK in Gibraltar and Akrotiri. Foreign politicians can demand that the UK abandon naval and military bases in the Mediterranean as the price for restoring customs-free trade in Great Britain. This is not a situation David Cameron should have allowed to come into existence. The Scottish Government has spent taxpayer’s money brushing off Freedom of Information requests asking what discussions they have had with Spain and Cyprus over this issue. Maybe those discussions didn’t happen either!

Scotland may well be better off outside the EU; after all, small non-EU states like Norway and New Zealand do fine, but pretending that the country won’t spend a day outside the EU is insulting to Scottish voters and the nation as a whole.

If you could bear reading this far, you should follow me on Twitter:

Istos custodes

Ofsted is now in a dispute with the Department for Education about no-notice inspections. Puzzled readers may wonder why any school inspection involves notice, for to give notice transforms the inspection regime from an enforcement mechanism to a protection racket: you can run schools however you want, but only if you’re organised enough to cover it up between notification of an inspection and clipboard hitting the desk two days later.

If you could bear reading this far, you should follow me on Twitter:

Not muddying the waters about Euroscepticism

The author of this Kosmopolit article makes the claim that it’s silly to label people or arguments using the terms “Europhile” and “Eurosceptic”.

That’s just wrong; the terms work perfectly fine, they describe whether someone favours the EU vis-a-vis the member states (or similar actors). If you want your country to leave the EU, you’re a Eurosceptic. If you want to repatriate powers, you’re a Eurosceptic. If you oppose the transfer or arrogation of new powers to the EU, you’re a Eurosceptic. The converse positions make you a Europhile.

Where it gets interesting (and in the Kosmopolit article, this is where the straw-man style argumentation and rhetorical questions all start to appear) is in two areas: internal conflicts between EU institutions, and situations where the EU does things that particular Eurosceptics support.

Eurosceptics are just not going to agree with each otherabout intra-institutional conflicts between Council, Court, Commission and Parliament. Why should they? It’s like asking people who favour labour against capital which side they back in a dispute between shareholders, board and management: their ideology just doesn’t discriminate at that level of detail, though individuals might have opinions on a general or case by case basis. It’s a matter of strategy and tactics, not an issue of principle.

Similarly, there will be cases where Eurosceptics are divided about particular EU policies, such as the Euro, surveillance, IP laws, etc. Ignoring the people who tactically support bad policies in the hope of hastening the EU’s demise, there’s no reason that people who want less EU power are going to agree on any other issue: Tony Benn, Margaret Thatcher, Enoch Powell, Michael Foot, Bob Crow, Nigel Farage, Dan Hannan, Dennis Healey, David Owen, and Kate Hoey are all over the political “spectrum”. It’s inevitable that the EU will often do things that some of them support. One principled view is to say that one opposes all exercises of competences that the EU should not have, and this is completely normal in the United States: Republican opponents of gay marriage nevertheless oppose federal bans on gay marriage on states rights’ grounds.

Once one has taken into account such positions, the Kosmopolit argument isn’t very convincing. He/she says “So just because I think the policy outcome is positive I am considered a “europhile”?”. A Question To Which The Answer Is No.

If you could bear reading this far, you should follow me on Twitter:

Other things Churchill supported

We’re often reminded that Churchill supported the ECHR or European integration more broadly, as though there were no better argument in favour or against these things.

For a bit of perspective, here’s a broader list of stuff Churchill liked:

  • “using poisoned gas against uncivilised tribes”
  • the Gold Standard
  • denying India’s right to be independent
  • using the army against strikers
  • politicians issuing orders to the police
  • the European Convention on Human Rights
  • European integration
  • imperialism
These people need some better arguments, or at least to explain why their cause gets to be associated with Churchill’s admirable qualities rather than his flaws.

If you could bear reading this far, you should follow me on Twitter:

Aliens don’t crash land

Today is the anniversary of the Roswell Incident, which is the subject of various conspiracy theories. I don’t like conspiracy theories; that way of thinking always tends to involve being selective about whether particular things are plausible.

There’s no reason to suppose that life necessarily exists outside our solar system, or that it is impossible for life to exist elsewhere, but that is not the point: we are invited to believe that intelligent creatures from outside our solar system crash landed in Roswell this day sixty-six years ago.

Is plausible that aliens could master interstellar travel, but not the ability to land without crashing?

If you could bear reading this far, you should follow me on Twitter:

The stakes of the EU debate just got a lot lower

We’re often told that the particular form of European integration we currently endure is somehow necessary for preventing another war in Europe.

Since Croatia’s accession last night, the cost of the most recent war in which EU member states were on opposite sides has now collapsed. Twenty-two years ago this week, Slovenia and Croatia fought on opposite sides of the Ten Day War which secured the former’s independence from Yugoslavia; no-one really wanted to be fighting, and the unhappy state of affairs constituted one of the least violent wars of all time: only 63 people were killed.

That magnitude of loss and foreshortening of human life is at the sort of scale that pharmaceutical regulators have to deal with when licensing drugs for use in the health system. In a world of finite resources and finite altruism, someone has to choose what drugs and medical procedures should be available at the expense of the taxpayer, and that means weighing the lives and health of different groups of people: if you have the cash to help either the diabetic or the woman with breast cancer, but not both, you have to have a reason for placing the life of one above the other. Just flipping a coin is morally repugnant. This is why we have QALYs.

A regulatory decision which makes drugs more expensive costs lives and suffering. Every time the EU’s deliberately undemocratic processes are captured by rent-seeking lobbyists trying to increase medical patent protection, there is a cost measurable in QALYs. Now when politicians raise the spectre of war to silence critics, those critics can say “well, the last war only cost 20000 QALYs, and your proposal looks worse”.

If you could bear reading this far, you should follow me on Twitter:

National Parliaments and EU Legitimacy

Jon Worth, Charles Grant and Ralf Grahn have been writing about the various options for giving national parliaments a role in the EU’s legislative process. This conversation between people who fundamentally agree that the EU in some form is desirable involves so many mistaken assumptions and false assertions that it’s impossible to deal with them all in a blog post of bearable length.

One feels like one’s wasting one’s breath even (re)stating all this but:

  • the EU won’t be legitimate until the people consent to its exercise of its current competences; what it will take to convince me that the requisite consent is present is a matrix showing, for every country C and subject S, that opinion polls say that the generality of people in county C are happy for their country to be bound by an EU-wide majority when laws are made about subject S; that’s how it works in real democratic federations
  • the “red card” proposals for national parliaments to have some role in blocking legislation only apply when the legislation violates the so-called principles of subsidiarity or proportionality, not when the legislation is outside the competence of the EU entirely
  • the EU does not have a demos, despite Mr Grahn’s reference to Miss Melchior’s assertion to the contrary. No test is suggested by either of them for how one might verify that the EU has a demos
  • vesting any sort of veto or consultative power in national parliaments is not going to improve input legitimacy
  • the best way to improve legitimacy is not to focus on outputs; there can be no such thing as a benevolent dictatorship, in theory or in practice; the exhaustive work of Bruce Bueno de Mesquita completely demolishes the case that it’s possible to improve citizens’ wellbeing whilst maintaining a kleptocracy
  • the democratic deficit is not a perception, it is a reality, and Mr Grant should concentrate on the wellbeing of actual voters rather than the opinions of the Quislington dinner party conversationalists to whom he seems to regard himself as exclusively accountable
  • unless “do you agree to be part of this country” is counted as part of “input legitimacy”, then the two-way split between input legitimacy and output legitimacy fails to capture a fundamental aspect of real political legitimacy. People in Ireland in 1918 and today in Northern Ireland rejected government from Westminster over any and all subjects; it was never the complaint that UK government was undemocratic, and if the EU were a democracy, many countries (more!) would still not want to be part of it
More seriously, adding national parliaments just adds more veto players; the problem is that people in individual countries don’t see it as in their interests to be bound by an EU-wide majority on almost any issue. The EU has already effectively arrogated to itself the power to legislate on any issue, but cannot get this ratified by the people, either incrementally or all at once.

If you could bear reading this far, you should follow me on Twitter:

First steps with Metametrik

Last weekend I attended the Open Economics sprint about Metametrik, which is an OKF project to help computers read the statistics in academic journal articles. Guo Xu posted a rough outline of what Metametrik should look like a year ago, but not much had been implemented.

We took an approach which turned out to be fairly similar to Guo’s recommendation: create a JSON schema capturing the basics of a regression result (the dependent variable, the goodness of fit, the sample size, standard errors and effect sizes of results), and then make tools which produce and consume data in this format.

So far, we have a tool which generates Metametrik format data, and a tool which reads this into a database. What’s needed next is web UIs that produce this data (for articles already published) and allow you to search it.

If you could bear reading this far, you should follow me on Twitter:

Doctor Who, the story so far

(Originally written 1999; updated for 2013).

I’ve been told I need to “lighten up”, so this blog post is a departure from my usual stodgy subject matter of the law-technology-politics interface, instead covering another thing which has fascinated me since I was a child: Doctor Who; I’m posting now, having almost finished work for the day, as in about an hour, they could well Spoil the show by revealing the Doctor’s name.

The last time this was about to happen was in the late 80s, when the Doctor was taunted about his identity by his enemies, and then asked by Ace who he was, and began “I am …”. But then the credits rolled. This episode, “Silver Nemesis”, was apparently supposed to end with the Doctor saying “I am Rassilon”, namely the co-founder of his planet’s society, and the writer for that episode didn’t know much about Doctor Who and thought the Doctor was God. Interestingly just before “Silver Nemesis” ends, the Doctor is playing chess, and lays down his king in resignation. This scene was paralleled last year in “The Wedding of River Song”, when again the Doctor is playing chess and strategically lays down his king. In the first story it was supposed to be an allegory for the crucifixion.

Who is the Doctor, and what is the Doctor?

Doctor Who as a story has lasted as long as it has because of its peculiar economics: the main actor playing the character can be killed off and replaced with someone else. The stories can be set anywhere and any time. This means stories in particular settings don’t need to introduce fresh characters each time, as we have the Doctor and his companions. There are a couple of other shows which work this way: the Goons and Blackadder spring to mind.

The other relevant economic aspect of the old series of the show is that it didn’t have a very large budget; this was part of its charm, but it also meant it couldn’t afford top flight producers, directors, writers, actors etc. Practically no-one involved in the old series is remembered for anything other than their connection with that series, except for the first producer, Verity Lambert, and Douglas Adams, who was script editor in the 1970s.

Inventing new characters and monsters and so on is expensive, and so the show gradually re-used monsters from its past (culminating in its 25th anniversay season where it did this every episode). You’d often notice a newly introduced monster, character or location would be back next season, and returning writers would bring their favourite monsters back with them. Eventually a couple of grand narratives emerged from the stories, and the show went on so long that three separate continuities can be identified:

  • the initial setup: we discover that the Doctor is not human, that he is instead a Time Lord living in exile and battling the Daleks and so on
  • in “Genesis of the Daleks” the history of the Daleks is rewritten, and the more interventionist part of the Time Lords’ government uses him as a somewhat willing agent advancing their agenda against the Daleks and other enemies; the Time Lords turn out to be rotten
  • from “Silver Nemesis” and “Remembrance of the Daleks”, it transpires that there is something special about the Doctor himself and not as he seems, but the show went on hiatus at this point

Beyond all this space opera tracery, what was fairly constant about the Doctor was that he would do what was right. He is supposed to be the good guy, and even when he is contemplating effective genocide (in “Genesis of the Daleks”) or murder (of the Daleks’ creator in a subsequent Dalek-related story), he was always clearly and thoughtfully doing what was morally right; the Third and Sixth Doctors were truest to this, often lecturing and hectoring people on moral grounds. In the original series, he always shown as fearless, though this is not true of the renewed series, which also gives him some sort of romantic life.

Politically, the Doctor seemed to have be a bit of a neocon, not the lefty that the media seems to have thought he was in “The Happiness Patrol”.

The new series has changed a lot of things: the production values are much better, particularly the writing, and the Doctor has fear and romance. What also seems to have changed is that there is supposed to be something special about the Doctor himself, as distinct from the Time Lords. He now seems to be of cosmic significance, which loses some of the original charm of the show, “but Doctor, the landslide will destroy the whole village!”. The new producer, who made the 1990s Comic Relief spoof of Doctor Who (in which the Doctor is played by Richard E Grant, and a woman …) loves getting characters to give long speeches saying why the Doctor is so great; these speeches are in “The Curse of Fatal Death” just as much as “Last of the Time Lords”, where they seem to have some sort of magical effect. Sydney Newman, one of the show’s co-creators, who’d never read Hamlet despite running BBC Drama, always said an serial should have only one unbelievable thing in it, and the new series depart from that seriously. The show needs to keep one foot on the ground.

There’s a much better environment now, too: the show was derailed in the 1970s by Mary Whitehouse. This censorious woman was engaged in a culturally destructive crusade, and stooped to bringing a criminal prosecution for sexual assault against a theatre director on the basis of eyewitness evidence obtained from someone sat in the back row. The BBC feared her, and she used her clout to get Doctor Who’s producer moved onto other projects. The show had been on a high, and never really recovered.

I hope the question marks remain about the man, and we don’t find out his name, or that Clara is the Doctor or is River Song or something, but we’ll see in a few minutes ..

If you could bear reading this far, you should follow me on Twitter: