Monday 7 December 2009

By Request: My thoughts on Perl 6

Good idea: Redesigning a clearly broken language from scratch

Bad idea:

multi unique (*$x, *@xs) { member($x, |@xs) ?? unique(|@xs) !! ($x, unique(|@xs)) }

Monday 5 October 2009

The bug-free myth: Why we trust verified software

Any time there is a discussion of formal proofs of correctness in software, I hear the same arguments made. These arguments are almost invariably made by people who have never done any formal verification, and who don't necessarily have a particularly good knowledge of how formal verification even works. This post will attempt to provide both a few counter-arguments against the usual objections, and an overview of the theoretical basis upon which formal verification of software depends.

The Bug-free myth

All too often, I hear the phrase "free of bugs" used in conjunction with theorem proving or formal verification of software. I want to make perfectly clear, this is not what theorem proving claims. You'll often hear phrases like "guaranteed correct". This is an (informal) shorthand for "guaranteed correct with respect to some specification". Allow me to make the distinction clear with an example.

Here is a program:

x = 0;
while(1) {
x = x + 1;
}
This program isn't very useful. It is not, however, incorrect (nor is it "correct"), without reference to some specification. If our specification is simply "keep incrementing a variable until the universe ends", this program is correct. If we were expecting this program to calculate something useful, or produce some output, then it is obviously incorrect. The "correctness" judgement always follows from a specification, and no judgement can be made in the absence of a specification.

This definition covers the (informal) usage of "correctness", but this is still distinct from "bug-free". The main activity within formal verification of software is generally the verification of specific safety and liveness properties.

"Safety" is approximately the guarantee that some bad thing can never happen. It might be that a certain storage location can never overflow, or that a value is always positive, or that a pointer is not null, or even much more concrete functional things, like "the autopilot will not switch off the engines while the plane is in flight". Keep in mind that doing nothing is always "safe". It's impossible for a storage location to overflow if the program never does anything. A program that simply halts immediately will fulfil almost any safety property you care to dream up, so we can re-state the definition as "if anything happens, it will be something desirable".

This is where liveness comes in. This is approximately the guarantee that "some desirable thing will happen (eventually)". These might be properties like "the doors will open", or "the value stored in X will be incremented".

When people talk about software being verified, they really mean that a set of safety and liveness properties have been shown to be true of the software in question. When undertaking a verification activity, we choose a set of safety and liveness properties that are of interest or importance, and we prove those. A property like "there are no bugs" is completely useless (and unprovable), however, for some safety property X, we can at least say "there are no bugs that would cause property X to become false".

One of the main ways we verify these safety and liveness properties is through the use of automated or interactive theorem provers. These are pieces of software that permit the construction of mathematical proofs, by both checking the proofs, and by providing some assistance to a human in searching for a suitable proof that some property holds. Unfortunately, as soon as you mention theorem provers and all the wonderful things they do, this usually leads to a new objection.

But what if the theorem prover has bugs in it?

OK, it seems a natural enough objection, but you don't think we're completely dumb, do you? For people in the business of proving software correct, you have to assume that we have some reason to believe the software we use is correct.

But actually, correctness within theorem provers is less important than you might think. I said earlier that a theorem prover has two basic functions - it acts as a proof checker, and it provides tools to aid in coming up with a suitable proof of a property.

The important part of this is that only the proof checker needs to be correct. The other parts of the theorem prover could just generate random garbage proofs, and they would be rejected as incorrect proofs of the property under consideration by the proof checker. In practice, the techniques used in proof search have some very good heuristics about the chance that they will succeed in finding a valid proof, and the time it will take for them to find such a proof, but these are just for the benefit of their users. These proof-search aids do not simply return "true" if they find a valid proof - they instead must return the proof itself, which the proof-checker can then verify.

So, hopefully you have been suitably convinced that most of the theorem prover does not need to be correct.

So how do you know that the proof checker is correct?

I'm glad you asked. This is going to require a quick whirlwind tour of how mathematical logic works.

Theorem provers like Isabelle and Coq have a wonderfully rich set of constructs built into them - numbers, arithmetic, records, functions - and the list goes on. The important fact about all of these things is that they can be constructed from a very small set of much simpler constructs.

There are a class of logics called Hilbert Systems that are built using a very small number of axioms and inference rules, and which permit you to build up most of the familiar constructs from logic and mathematics in a systematic way. Similarly, Zermelo–Fraenkel set theory also allows one to build up almost all of mathematics in a systematic way. This is old magic, and it is pretty well understood.

Because I'm writing this for a general audience, I don't feel the need to scrape the depths of my own knowledge to come up with the specifics of the logical foundations used within specific theorem provers, but if you get the general idea that there have been many attempts to formalise all of mathematics from a very small set of core constructs, and many of them have been successful enough to give us a formalised foundation for the types of mathematics most of us care about, then you already know how a theorem prover works.

So once we've encoded this very small core manually, we can build all the rest of our theorem prover theories from this small core. We can mechanically check that we are doing this right, either by hand, or using various automated proof-checking techniques.

The small core inside the theorem prover is all that is really important now, in terms of correctness. This can be verified by hand, and it can also be verified using other theorem provers.

But even this doesn't really need to be correct. When we use a theorem prover to aid us in proving a property, we end up with a proof script - some machine-readable version of the proof. This doesn't necessarily rely upon the software that was used to help create it (although it might get messy trying to decouple it). This proof can be verified using any other piece of software, or it can be verified by hand without any creativity - you just have to mechanically apply each step in the proof and satisfy yourself that each step follows by a valid step of inference from the last.

The final important property of theorem proving software is that we can always look for consistency. If we get anything wrong anywhere along the way, proofs are going to start failing. It is already true that there are some valid statements that cannot be proved to be true in the logic in question, but this isn't really a problem as far as the correctness of the theorem prover is concerned. We would only be concerned if there were false statements that could somehow be shown to be true inside our logical system - and this is not the case! It is erroneous to prove a contradiction, so if this happens, mechanical proof checking will reject the proof.

But what if the proof has bugs in it
?

Hopefully you are satisfied that we can have a very high degree of confidence in the results we get out of a theorem prover, so a proof is not like a "program" in the sense that we can have valid steps of reasoning and just "get the wrong answer". The only place where real "bugs" can be introduced is in the human side of things, where we choose the wrong safety or liveness properties that do not actually capture the properties we are interested in.

There are several strategies that we can use here. The first is syntax and type checking on the specification itself. Given that we are expressing our safety properties inside a theorem prover using something that is essentially a programming language, we can use the same techniques that have been shown to be very useful in enforcing consistency and detecting errors in traditional programming languages. This should remove the possibility that a simple typo could be totally catastrophic.

The second way is enforcing a discipline where we re-state the same properties in different ways. By doing this, we ensure that either a proof of one of the properties will fail, or we will introduce inconsistency between our encodings of the properties which will be rejected by the theorem prover.

Finally, and although I've previously argued against it, be careful. This is very different to the suggestion that you just "be careful" when constructing a program in a traditional language. This is about a set of safety properties. You can only guarantee that your program is correct with respect to the specification that you have written down. If you are falsely claiming confidence in your software where none exists, then that would be just as catastrophic in any environment. I really think it's worth saying here that we are way off into the land of the abstract. Even in a complex specification, it would be very difficult to encode things in such a way that you succeed in proving a whole set of properties, none of which provide the guarantees you think you are making (the proof is likely to fail if you have an inconsistent model of what you think you are proving and what you are actually proving). This is a much stronger safeguard against human error than is provided in any traditional programming environment available today.

But what if the compiler is incorrect?

There are two basic counter-arguments to this. Basically, in proving properties about software, you are either working with an idealised model of the software encoded into the theorem prover assuming some particular semantics for the target language and/or underlying hardware, or you are actually writing the software inside the theorem prover, and then generating code once you have proven all the properties of interest. In either case, you are somewhat at the mercy of compilers. This is always the case though - any correct program could be made incorrect if there are faults in the compiler or the hardware. You can take two approaches here - assume that the hardware and compiler work as expected (therefore invalidating your guarantees of correctness if they do not), or make use of the recent work on certified compilation to at least remove the uncertainty of the compiler from the equation. There is a whole different body of work on (hardware) fault tolerance in software. If you're really getting to this level of safety, then you probably need to be an expert on these kinds of issues anyway. Theorem provers for software verification are concerned with the verification of certain properties. If validating your assumptions about the hardware and software environments are important, then you will need to do more work.

Is it worth it?

For some things, yes. This kind of formal software verification is hard work. It's very labour intensive, and it requires a great deal of effort. That said, it is getting easier as the tools get better, the barrier to entry is getting lower. I don't think it will be very long before we start seeing a lot more in the way of light-weight theorem proving taking place as a standard part of compilation. In a world where software failure costs huge amount of money, it doesn't seem so remote a possibility that it will become practical and cost-efficient to apply formal verification to more software.

--

Personal plea: I'm still looking for reasonably-priced accommodation for my partner and I in Copenhagen if anyone has any leads. I'm eager to go start my PhD at ITU, but need to find somewhere to live first.

Friday 2 October 2009

Insecure software is your fault

Security breaches in software are really just a special case of software failure, but it has the dubious honour of having a "community" build around it. There is a cost associated with all software failure, but most people are willing to tolerate a certain amount of failure in their applications - as I'm often reminded whenever I discuss formal methods with other programmers - "mostly working is good enough". I can understand this viewpoint (although I don't agree with it), however by this reasoning, what is the acceptable level of security vulnerability in software?

You can tolerate your word processor crashing every few days, but is it acceptable for your entire customer database to be stolen once every few days? How about your production server being rooted once a month? A crippling worm attack once per year? Where does the cost/benefit relationship come into play here?

I don't believe that anyone would seriously advocate the position that a serious security breach once per year resulting in data loss or theft is "acceptable". I doubt anyone wants to have to pay for system administrators to reinstall compromised machines once a month.

The title of this article is "insecure software is your fault". I use "your" to refer to developers. I'll expand on this towards the end of this article, but basically, I believe this to be the case because we have the tools to eliminate most kinds of software vulnerabilities, and yet they still exist, because programmers continue to not employ any of these tools or techniques. If you aren't a software developer, or you actually use the best tools and practices available to you to produce good software, then you can safely assume that I don't mean that insecure software is your fault.

I should create some distinction here between two different types of software "insecurity":

1) Flaws and defects caused by language-level features such as manual memory management or insufficient sanity checks on input that permit damage to data or unauthorised access at the same privilege level as the program itself. SQL injection and some buffer overflow attacks would seem to be obvious examples of this kind of thing.

2) Flaws or defects caused by deficiencies in design - i.e., the software is unable to be compromised itself, however it enables undesirable actions within the application itself. Cross-site scripting attacks are the most obvious example of this - the browser itself remains uncompromised, but any data inside the browser is basically at risk due to an inadequately designed security model.

In the first class of vulnerabilities, there are language-based solutions. Type safety guarantees are sufficiently strong to prevent most kinds of attacks that rely on runtime type violations to exploit flaws. Removing manual memory management from languages reduces another huge class of possible errors. Automatic bounds-checking is the third and final part of it. Contrary to popular myth, the performance cost of these things is very small, and yet the benefit is huge. You've just eliminated even the potential to inadvertently expose yourself and your users to a huge class of security vulnerabilities that will cost time and money to fix.

Claiming that you don't need any of these catastrophe-preventing measures because you're careful is a weak excuse. It's a weak excuse because every experience we've had shows us that being careful just isn't good enough. Suggesting that any developer who has ever introduced a security flaw just wasn't careful enough is a hugely arrogant assertion. If you accept that security vulnerabilities can happen to people who are both smart and careful, then why can't they happen to you? You have a responsibility to your users to be more than careful, you have a responsibility to be sure. And using language-based features that remove a huge class of potential errors is a way to be sure.

In some rare circumstances where performance concerns actually dictate that you must not use these features, don't write a network-facing service. The only place I suggest being careful is in isolating potentially insecure software from the outside world.

There is a small caveat to this - not all languages were created equal. In some cases the design of the language may be sufficient to remove a large class of vulnerabilities (through automatic memory management, bounds checking and sensible typing strategies), however in the interpreted case, you are essentially at the mercy of the interpreter. Your code may be perfectly sane, and the language may be sane, but the interpreter written in C isn't necessarily sane or safe. I add this only as a caution, because the same could be said of the operating system or even the hardware platform - you're only as secure as the things you rely upon. However, anecdotally at least, it's very rare that operating systems have vulnerabilities that are likely to be exploitable only within your application if your application is otherwise defect-free, whereas this isn't always the case with network-facing interpreters.

The second class of errors I identified is errors caused by flaws in design. These can involve things like leaving scope for protocol violations, insufficient security models and some downright stupidity. Very few of these situations have an obvious "language-based" solution at this moment. If your application-level security model is flawed, the language-based features aren't going to help. If illegitimate users of the application are able to cause mischief without ever "exploiting", then the security model is flawed. This could be as simple as leaving a "delete" action outside of some authenticated realm (allowing unauthenticated users to delete things they shouldn't be able to), or it could be that a specially crafted series of actions leads to an undesirable or inconsistent state.

Whatever the specifics, these are all essentially safety properties, as in "this software is not able to exhibit these undesirable behaviours". We actually have ways of checking safety properties nearly automatically these days. You can check various properties through model checking. You can build things inside theorem provers and prove safety properties. Tools like Daikon can even aid in the generation of various invariants through runtime analysis. ESC/Java2 can check certain kinds of safety properties at compile time. BLAST works on C programs. Spec# can express various safety properties, and there are hundreds more similar efforts.

Basically what I'm getting at is that these tools really aren't impossible to use, and they can give you concrete guarantees where you might otherwise have just been guessing. The main thing is the ability to ensure a globally consistent view of the implications of any design decision relating to security. I've previously asserted that humans aren't very good at keeping globally consistent mental models of complex systems, hence why I (and many others before me) advocate mechanical approaches to ensuring global consistency.

So the take-home point from this (rather long) article is that we actually have the tools right now to eliminate most of the kinds of security vulnerabilities that exist. The problem is that people aren't really using them in many places where they really should be. The much-reported damage caused by viruses and worms and "crackers" and DDoS attacks and zombies are all the direct result of insecure software. Sure, people who engage in those sorts of activities are criminals, but really, we're basically leaving our doors and windows wide open and yet we still seems surprised when somebody comes in and steals stuff. If anything, I think we should all start to mentally substitute the phrase "damage caused by cyber-criminals" with "damage caused by irresponsible software developers".

If you happen to be a "computer security professional" (scare quotes intentional), then perhaps you can educate me as to why anti-virus software and firewalls and chasing endless exploits through ad-hoc "penetration testing" is still regarded as the primary activity of the "security community", rather than actually making serious efforts towards preventing security defects in the first place. I have my own pet theory (spoiler alert: $$$), but I'd be interested to hear more informed opinions.

--

As a side note, I can now announce that I've accepted a PhD position in the PLS group at the IT University of Copenhagen. I'm currently looking for a place for my parter and I to live in Copenhagen from the start of November, so if anyone from Denmark reading this has any leads, please let me know!

Wednesday 30 September 2009

Bletchley Park

Rare non-PL post, but I figure this one is worth it.

I went to Bletchley Park last weekend, and had an absolutely fantastic time. There was a lot more there than I expected. It's an absolute bargain at £10, and it's only about 45 minutes on the train from Euston station in London. It's definitely worth doing one of the free tours, too. The guides are extremely knowledgeable and entertaining.

Also located there is the National Museum of Computing, which was fascinating. I took some pictures:


And one of me standing in front of a PDP-11 looking quizzical:



























So, if you are in the UK, or are planning a visit, definitely make the effort to get to Bletchley Park.

Thursday 24 September 2009

Two features that would improve my life

If you've ever seen From the Earth to the Moon, you might remember the episode about the creation of the Lunar Lander. Tom Kelly is shown standing outside throwing a red ball against a wall repeatedly while he tries to think of solutions to hard problems. This scene has always been memorable to me because I think it is the only cinematic depiction of "problem solving" that has ever seemed familiar to me.

I cite this scene because it echoes the way I problem solve. I think a lot, and I do strange things in an undirected manner until I solve it. When I'm actually creating software, I generally know how most of it is going to work before I even start typing. Writing all the supporting code and boilerplate is not intellectually challenging - and I think this is the majority of the "programming" that a commercial programmer is called upon to do.

In the midst of this programming-as-typing though, there are often hard problems that need to be solved. These are usually the bits that I find myself actually needing to think about - they are usually hard problems to reason about, and I find that I "code around" them in many instances. It's the kind of situation where you might write a stub and then promise yourself to come back and write it later, once you understand the problem (and its solution) a little better.

A recent example for me - I was attempting to figure out how to do a novel kind of type inference over complex terms. I wrote a "infer" function that takes a piece of a program and returns a typed piece of program. And then I wrote some tests, and my implementation consists of just returning "unknown type". Not very useful.

I have a bunch of strategies I usually use when I'm trying to solve these kinds of problems. I scribble on paper a lot, trying to contrive concrete examples that I can start to generalise into an actual algorithm. That's fine at the early stages, and helps my understanding a lot.

Another strategy is to use some sort of REPL (interactive environment) and try to write bits of code that get me closer to my goal. I usually use MLton for development, so this usually means switching over to SML/NJ so that I can start to "sketch" in code.

Often these two approaches are enough to get me most of the way to a solution. If the problem is really hard, it might not be. In these cases, I generally wheel out my trusty theorem prover, Isabelle. At this point, it becomes possible to re-implement the bits of supporting code that I need in order to express the problem, and then start trying to test my assumptions by actually proving properties about the kinds of functions I'm "sketching". This forces me to make very concrete my assumptions and intentions, because a theorem prover refuses to make educated guesses.

So, having gone through that entire process, I was thinking of something that would make my life better: a language-aware prototyping environment.

Let me explain. I have very little tolerance (or desire to use) visual programming environments, or "CASE tools", or very dynamic languages that permit "rapid prototyping". I'm talking about something that will help while I'm trying to solve hard problems embedded within lots of other code during "real" software development.

Basically I want the ability to access all of the supporting code and boilerplate that I've written in order to express my problem from within a prototyping environment. Having to re-implement things inside Isabelle is a pain, particularly if I'm dealing with problems that are linked to the way things are represented. I have to re-build all of the structures in another language just to be able to re-state the problem I'm trying to solve.

So I want to be able to instantiate a prototyping environment exactly where I would currently just write a stub. I want to be able to see visualisations of data easily. I'd like to be able to do some of the things that I do with the REPL. I'd like to be able to easily save and re-run test cases. So far, so pedestrian.

And this is where it starts to get more interesting. I want to be able to write partial specifications. In this kind of "exploratory programming" - I want to be able to start to apply "fuzzy" constraints until they become clearer in my head, mixing them with valid program code. I think a good way to do this would be to employ some of the techniques from Qualitative Spatial and Temporal Reasoning. These could be quite simple things, for example: "this value gets bigger over time", "this event is going to occur before this one", and when dealing with complex data structures - "this value exists inside this other one".

None of this would be directly executable, naturally, but with a range of visualisation options and some consistency checking, it would give you an ability to interact with a partially-written program in ways that you would otherwise start to do manually in a REPL. Taking some of the QSTR statements and deriving some new facts from them would be useful too - if I have a bit of code saying that x gets bigger over time, then perhaps it could tell me that this means that y will get smaller over time. It could draw me a pretty graph! By being able to mix "real" code with these kinds of qualitative statements, I think you could start to get some interesting results. I think the trick would be to integrate it into a compiler so that it's not necessary to do this in a "dynamic" way - the stuff that is not directly executable just gets compiled into some code that implements the prototyping environment.

That's the first feature that I think would improve my life. It would serve as a (metaphorical) "red ball" to throw against the wall while you try to solve a hard problem.

The second is a fairly simple extension: generate tests, specifications and documentation based on this prototyping process. By including your compiler in the prototyping process, it seems like you are actually starting to capture a whole bunch of useful information.

If I specified that A comes before B, then surely there are some useful tests (what happens if B comes before A, for example?). If I made some statement about the depth of a tree versus the number of iterations through a piece of code, then that might be an interesting test or profiling metric.

From a documentation standpoint, it seems like you could generate some useful documentation that provides insight into how a "difficult" piece of code actually works, because hopefully it would be possible to capture some of the rationale and the intuitive problem solving process that led to the eventual solution. By keeping track of the revisions made inside the prototyping environment, you essentially have a record of the "story" of the code as it becomes more concrete.

While it would probably be a reasonable amount of work, it's certainly not impossible. I believe the minimal set of functionality that would actually make this a useful feature would be quite small. I think this could be a "killer app" for some programming language - as long as the rest of the language was sane, I think I could be convinced to make a switch.

Monday 14 September 2009

Pigeons and Programming: Superstitious behaviour

You may be familiar with B.F. Skinner's experiments with pigeons, published in 1948. Basically, pigeons were kept in cages and fed on random schedules. This led to the pigeons developing some rather bizarre behaviour - turning in clockwise circles, attempting to "lift" an invisible bar, and various other odd actions. Skinner's conclusion was that this kind of reinforcement led to a kind of weak association between whatever the pigeon was doing when food was delivered and the "reward" of getting food. The eventual conclusion was that these pigeons were displaying a kind of "superstitious behaviour", which led them to repeat actions that resulted in reward in the past, despite there being absolutely no causal effect.

Some psychologists object to extending these results to an explanation for superstitious behaviour in humans, but I believe the link between reinforcement and repeated behaviour is relatively well-demonstrated.

What's the point of this pigeon story? I think it applies to programming.

Having a poor mental model of the semantics of a programming language leads to all sorts of bizarre superstitious behaviour. You only have to read thedailywtf for a little while to see all kinds of examples of the programming equivalent of throwing salt over your shoulder and turning around three times. Let me stretch the analogy a little further:

Certain programming structures lead to success in a task. This success leads to a kind of reinforcement of the techniques used to reach that solution. This "reinforcement" could be compiling, passing tests or running successfully. Similarly, there is a kind of negative reinforcement schedule - compile errors, failing tests or runtime failures.

It's important to form a distinction at this point between simple learning-from-experience and the kinds of superstitious behaviour that I'm arguing occur in programming. Let me give an example - having a poor knowledge of a given language, let's say that I construct a program and I apply techniques A, B, C and D. These could be anything, really - naming schemes for variables, grouping of sub-expressions with parentheses, adherence to particular patterns, or anything else. It may be that only A and C were sufficient in order to have the program compile and run. Unfortunately, I've also included B and D. Next time I come to write a program, if I continue applying B and D, these become a kind of entrenched superstition. They serve no purpose, except to make reading code more difficult for programmers who do not share your superstitions. This is still just learning from experience though - this isn't inherently "superstitious" - it's just a school of programming associated with throwing everything at a wall and seeing what sticks.

Now, here's the crux: it is inconsistent application of "reward" that leads to superstitious behaviour. This inconsistency exists in two basic forms in programming languages. The first is when there is a lot of hidden behaviour. When there are a lot of hidden assumptions, it becomes very difficult to discern why your program works. This is where the compiler or framework takes on a "magical" quality, whereby the rules governing success or failure are so complex as to seem almost random.

The second opportunity for inconsistent application of reward is late failure. I find this kind of behaviour is regularly present within the high-level, dynamically-typed, interpreted languages. Where the goals of these languages emphasise being accessible and intuitive for beginners, this actually equates in many cases to "keep running until the error is completely fatal". Where failure occurs well away from the actual source of the error, diagnosing and correcting errors can quickly become an exercise in near-random mutation of source code. When cause-and-effect become very difficult to predict, then changing one part of the system and having another piece break (or start working) becomes a kind of reinforcement schedule. This has two dangerous impacts: 1) it leads to unnecessary error handling in places there shouldn't be error handling. The hideous global "try/catch" block wrapping an entire program is a symptom of failure occurring much later than it should. 2) programmers become timid about touching certain parts of a system. This leads to more "magical thinking", whereby a piece of the system not only is difficult to understand, but should not be attempted to be understood. This makes it almost impossible to refactor or grow a system in a structured way. There will always be bits of "magical" code waiting to break unexpectedly.

So of the two sources of inconsistency, the first is the easiest to address. This basically just corresponds to "learn enough about your environment so that it no longer appears magical":

  • Test your assumptions regularly - Do you really need those extra parentheses? If you're not sure, try it without.
  • Be a square: read the manual - it seems incredibly dull, but it's actually worth understanding your language of choice from the ground up. You may be a good enough programmer to pick up languages just by reading a bit of source code and a few ad hoc tutorials, but there is something to be said for the systematic approach to learning a language - namely, the hidden behaviours of the environment become considerably less magical.
  • Avoid magic - If you're considering web frameworks or programming languages or whatever, beware the phrase "it all just works". If you don't understand how or why it works, and you don't believe you are willing to devote the effort to understanding how or why it works, then the benefits of any whiz-bang features are going to be eaten up by the maintenance and correctness issues you'll suffer as a result of superstitious behaviour.
The late failure issue is considerably harder to address without simply suggesting switching to a language that can enforce certain properties and that will fail early. By "early" I mean, "at compile time" or "immediately after the first error case". I am always particularly suspicious of languages where things like silent type coercion and silent initialisation of never-seen-before variables occurs. These are basically just error cases waiting to happen, but they won't be revealed until much, much later in the execution of the program. When a typo at line 1 can cause an incorrect result at line 10,000, you probably have a problem.

So the only advice I can offer, aside from "fail early" is to employ self-discipline in the absence of language-enforced discipline. Attempt to build structures that will cause your program to fail early rather than deferring failure. Avoid developing superstitious behaviours around certain pieces of code - if everyone spends a little time questioning their own attitudes towards development (and particularly towards debugging), then maybe there will be a little less superstitious coding behaviour in the world.

Monday 7 September 2009

Why programming language design is hard (and a few ways it can be made easier)

When designing a programming language and accompanying implementation, you are forced to keep thinking at three different levels - the way that the implementation works, the way that people will use it, and the requirements that influence design decisions.

On the face of it, this is no different to any other software development activity. In building a stock control system or any other common piece of software, I would be forced to think about the way it will be used (e.g. how users will enter items and how the people in the distribution centre will scan items as they leave), the implementation (e.g. what classes/functions/methods implement this functionality) and the requirements influencing the design (e.g. Mr. Big Boss of International Corporation really wants the software to be beige).

The difference with programming languages and many other types of software implementations is that it is difficult to relate your requirements and design decisions back into the real world. When designing a stock control system, a stock item is designed in such a way that it is some representation of a real item in a real warehouse. The behaviour of the system attempts to reflect real processes carried out by real people. You can go down and meet the people who dispatch the items if you want, and ask them all about their jobs. Having these two very concrete things at your disposal makes implementation correspondingly easier, because you have a "real world" system against which to validate your software system.

Programming language design lacks these analogous constructs. The "behaviour" of the programming language basically corresponds to the semantics of the language, which you're probably still trying to nail down (it's unlikely that you have a written semantics, right?). The way the users are going to make use of your programming language depends on what the semantics are. While you can contrive examples and try to implement them in the language, you lack perspective, because the semantics that you have implemented are exactly the way they are because they correspond to your understanding of the semantics. You're probably the person worst-equipped to make judgements about the usability of your own creation. This removes our two best tools for guiding an implementation; the ability to predict users' behaviour with respect to the system, and concrete things against which to verify our assumptions.

A few solutions

1) Get feedback early and often - this is important in all software development, but if you are designing a new programming language, you need to be talking to people all the time. While some people you talk to will demonstrate objections on some sort of dogmatic ideological basis ("I don't like static type systems, and you have a static type system, so the entire language is junk"), explaining the semantics to other people and gauging how much effort it requires for them to get a sense of the language will be very helpful in guiding future decisions.

2) Know why you're designing a new programming language - novelty or fun are perfectly valid reasons for doing PL design, but never lose sight of the fact that almost nobody will use a new programming language unless it does something better/easier/faster than they can already do it in one of the 10 trillion programming languages in the wild today. Think about the kinds of programs that you want the language to be able to express easily, and what kinds of programs will be more difficult to express. You might be aiming to create a general-purpose programming language, but that doesn't mean it's going to be good at absolutely everything. If you do claim to be designing a general-purpose language, here's a good thing to keep in mind at every point during your development: "How would I feel about writing this compiler in my new language?"

3) Write things down, often - Your ideas will probably change the more concrete your design gets. As you start being able to interact with your design (because you have a partial implementation of an interpreter or compiler), you will probably change your mind. Writing down a description (formal or informal) of your syntax and semantics will help keep you from completely contradicting your own stated goals. If (as in point 2) you decided that you were designing a language that would be good at expressing programs of type X, and then you subsequently make some changes that make it very difficult to express those types of programs, then what was the point of your language again? Keep referring to point 1.

4) Write tests - however sceptical or enthusiastic you may be about test-driven development in other endeavours, I can't stress enough how useful it is for programming language design. At the very least, keep a directory full of the test programs you write and automate some means of running these. If you can write tests down to the statement level, do that. You can never have too many tests. As I said in point 3, your design is likely to change. You need to be bold in refactoring and redesigning, otherwise your ability to change fundamental design decisions will suffer. You'll end up building "hacks" into your syntax or semantics just because you really aren't sure if changing some assumption or construct will break everything. This has the added benefit of providing you with a whole lot of sample code when you come to write documentation.

5) Think about the theory - Don't be afraid of theory. Theory is your friend. A lot of people have published a lot of papers on many facets of programming language design. It's worth learning enough about the theory of programming languages to enable you to read some of this published output. If you're stumbling around in the dark trying to figure out a way to statically enforce some property, or a more efficient register-allocation algorithm for code generation or just trying to figure out why your parser generator is complaining about your grammar, chances are that somebody has solved this problem before, and has expressed some solution to it in a published form. You'll find it much easier to relate the constructs in your new language to other existing languages if you don't reinvent the terminology wheel too. I can't recommend strongly enough Types and Programming Languages by Benjamin C. Pierce as an excellent starting point for all things theoretical in the programming languages world.

6) Consider using ML - I wouldn't be the first to note that ML is really good for writing compilers. Obviously, your circumstances may be different to mine, but having written compilers and interpreters in a few different languages, I haven't found anything quite as good as ML at expressing the kinds of parsing, validation and translation activities that are integral to compiler implementation. The type system helps prevent the majority of errors that you are likely to encounter while writing compilers. Recursive data types express most internal compiler structures perfectly, and the presence of mutable storage and imperative I/O means that you don't need to jump through too may "functional programming" hoops in order to achieve some of the things for which those features are useful. Also, the very existence of Modern Compiler Implementation in ML by Andrew Appel (which I consider to be the best introductory text on compilers to date) should make you at least think about having a look before you decide on an implementation language for your next compiler.

7) Don't be afraid of being the same - There is a tendency towards ensuring that your syntax and semantics are different from everything else in existence. If language X has a feature that is similar to yours, do you really need to invent new syntax and terminology? If something exists elsewhere, it's probably worth your time to figure out how it works and how it is expressed, and then re-implement it in a way that would be familiar to users of language X. If you are actually interested in having people adopt your language, then you should reduce the learning curve as much as possible by only inventing new terminology and syntax where it is appropriate to do so (i.e., because it is either a novel feature, or there is some improvement that can be made by doing it differently). If you're creating a new language, you've already established that there are things you can do differently or better, so it's not necessary to go overboard in differentiating yourself. If it were, PHP would never have become popular in the presence of Perl. Clojure and Scheme would never have survived the disadvantage of Lisp already existing, and so on.

Having laid out all of these points, I'm certainly guilty of not taking my own medicine at times. I've largely written this out because I'm currently going through a design and implementation process with Lope, and I don't want to repeat my past mistakes!

Thursday 3 September 2009

On the semantics of pseudo-code

I was reading a thread on HackerNews entitled "What language do you think in?" and I was fascinated by the responses.

Many of those commenting claimed to think "in pseudo-code". That got me thinking - what does it mean to think in pseudo-code?

By the textbook definition, pseudo-code is some sort of idealised, abstract code with an informal syntax. It serves as an aid to human understanding, making use of the abilities of humans to resolve ambiguity in a sensible way and "black box" a lot of minor details. That all sounds fine.

The catch for me comes in thinking about the semantics of this mental pseudo-code. It still has some semantics, I assume, otherwise it is likely to be entirely useless as a mental model. Perhaps we think of a statement in pseudo-code for "sum all of the values in X":
for each value k in X
a = a + x
OK, so that seems a reasonable enough translation from an English language specification into some code. We've left out some details like what the initial value of "a" is, and the syntax is pretty fluid, but it should be unambiguous to most readers.

The problem is that this is only one step of nearly-mechanical translation from just writing code in a programming language. There is a sneaky step of concretisation going on here, both in the framing of the statement, and the pseudo-code representation.

First, in the framing of the statement, we've assumed a stored list of values exists and is called "X". Even abstracting this away to "the list of input values" (referring to it by its purpose, rather than a label) is still commitment to a paradigm at this early stage. On the language side, we've basically just taken the semantics of some reasonably ubiquitous "C-style" language (think C, Python, Ruby, whatever) and abstracted away some syntax. This really doesn't seem very useful in terms of "abstract thinking".

So is this really what people mean when they say "thinking in pseudo-code"? If so, that's just really a coded way of saying "I mentally construct programs in an idealised version of language X", where 'X' is some language (or perhaps group of similar languages) that the programmer is familiar with.

I'm really not a fan of early concretisation. I can't think how many times I've been in a meeting discussing high-level requirements with a group of technical and non-technical people. The conversation goes something like:

Non-Technical Person: We're really going to need X
Me: Are you sure you need X? Y seems to do everything you want equally well, and it might fit better with the established processes of the organisation.
Non-Technical Person: The processes that are important are...
Technical Person 1: ... we should do Z! because there will just be a couple of classes to add, and using language version 2.3.7 we can just use built-in serialisers to create an object store.
Technical Person 2: No, 2.3.7 will require a kernel upgrade, we should use 2.3.6 and avoid that altogether.
(...)
Me: *head explosion*
Names and specifics (and a little dramatic effect) aside, I've really had this exact conversation more than once in more than one organisation. What I've come to realise is that there are a lot of people who refuse to engage in a conversation in the abstract, and they have to mentally compile to code or implementation details in order to even engage with the conversation. I think this is probably the result of people who genuinely do think in pseudo-code in the way that I've described.

Naturally, this is all speculative, because I'm not sure I could force myself to think in code if I tried. I'm just not wired that way. I need to have a high-level understanding of a problem (which allows me to mentally formulate a high-level solution - usually in terms of the same abstract concepts used to describe the problem), and then "programming" becomes a typing exercise, in which I mentally translate from a high-level computational model to the code I'm writing as I type it.

So, I'm interested in hearing from people who do claim to think in 'pseudo-code'. Have I completely misrepresented what you mean when you say it? Are you actually writing in a language with syntax in your head? Do you close your eyes and see functions and objects and whatever else? Similarly, if you don't think like that, have you observed others that do?

Monday 31 August 2009

Making money from programming language design

I've had an interest in programming language design for a long time. Lately, however, as I've been working on my prototype bigraphs-based language, I've been pondering the economics of programming language design. Not that I have ever been particularly interested in making vast sums of money from designing programming languages - I'm much more interested in solving interesting problems, but it's interesting that PL design is viewed as a bit of a poor cousin to other varieties of mad schemes. You're a startup with a $100k/month burn rate designing a new Web 2.0 application that will simultaneously topple Facebook, Spotify and cure cancer? Sure, sounds exciting! You're designing a new programming language? Oh, it'll never catch on.

The lack of enthusiasm from those outside the PL design community probably stems from the fact that it is probably a bit of a lame duck in terms of earning money*. I do it for fun and interest (and making the world a better place etc), but that argument doesn't fly with some people.

* I know, there are lots of other reasons. The strange ways in which adoption and rejection of languages by users works would make me nervous if I were an investor. Also, sometimes it's hard to get enthusiastic about conversations over the merits of particular syntactic constructs.

So this post is dedicated to various ways that it might be possible to make money from programming language design (and implementation). There is probably a large overlap here with the economics of software in general. This is largely hypothetical, as I can't say that I've succeeded (or even tried) in making any significant amount of money from programming language design. Similarly, I'm basically "thinking out loud" at any scale. Some of these ideas might work to earn some beer money for one guy in a garage, while others might only be achievable by huge corporations with millions of dollars of contracts. Either way, my point is to simply enumerate some ways in which programming language design and implementation itself could be financially rewarding.

1) Commercial compilers

By "commercial compilers" I mean you create a single reference implementation that is "the compiler", and then you sell licenses for the compiler software. This is probably not a serious option outside a few specialist domains, given the myriad of production quality compilers for most languages, almost all of which are free and open-source. This might be an option if you are targeting some very specific (and probably very expensive) piece of hardware, especially if your language provides some value that the vendor-supplied implementation does not. The "specific" part is probably the important part. In the absence of other options, people become much more willing to part with money. If they can just use the same open-source compiler for the same old language they've always used, they probably will.

Incidentally, I am interested to know how the economics of the entire .NET thing has worked out. I assume Visual Studio is still a commercial product? It's been several thousand years since I looked at it. I assume the incentive for the creation of C# was not to profit directly from the language, but rather to create a big vendor lock? The existence of Mono creates an even stranger situation. If you know more about this side of .NET than me, I'm eager to learn more.

2) Free compilers, commercial add-ons

This is a pretty simple model. Open source the compiler, then sell value-added IDEs, debuggers, accelerators, static analysis tools and anything else you can think of. My understanding is that this is largely the route taken by Zend. It's probably not a bad approach, weakly corresponding to the "the first hit is free" school of business employed by many entrepreneurs working on street corners. In a situation where you control the language specification, and the implementation, then you are likely the best-positioned to create accompanying tools that "professional" users of the language are likely to want or need. This permits people to become fully familiar with the language as a hobbyist, producing real (useful) software using the freely available tools, and then moving on to commercial programming environments where the cost of tools is hardly considered.

Personally though, I'm pretty stingy when it comes to buying software that I don't really need. Commercial IDE? I don't use IDEs anyway. Commercial debugger? I'll do print-debugging if I have to. The "our implementation is crap unless you buy X" stuff is pretty much an automatic way of making me not give your language a second thought.

3) Sell support

You know, the old open source trick. I have no interest in the debate as to whether this is commercially viable or not, but it seems to work for some people. I'd rather not. I assume this would essentially equate to some kind of commercial support, either becoming a producer of software in your language, or providing training and tool-support services. This might extend to providing some kind of certification process for programmers.

4) Domain-specific embeddings

Domain-specific languages are hot right now. I quite like the idea that a single language design could then be specialised into domains in exchange for money. I think the key difference between making money from programming languages and software in general is that people are almost completely unwilling to pay for compilers or tools for general-purpose languages. There's just no need in this day and age. However, within a domain-specific context, it would appear that there may be more acceptance and willingness to pay for tools and support. It might be that you can convince large company X to pay you to create a DSL for their particular domain, or it might simply be a matter of convincing users of your general-purpose language that their particular task would be easier/better/faster in some domain-specific variant that you sell.

5) License the spec/controlled membership

Form a consortium! Charge bucketloads of money for interested parties to become members. You probably need a lot of users with a lot of money (read: "enterprise") before this would cease to be a joke. If you could get into this sort of situation, you're probably already making money from your language in one way or another. Licensing the specification, certifying implementations, and simply collecting fees for pretty much anything sounds appealing.

6) Write a book

I know even less about the economics of publishing than I do about the economics of programming languages, but I assume the fact that people continue to publish books mean that someone, somewhere is making money from them. Writing a book about your language seems to be a good way to kill two birds with one stone (i.e. write good quality documentation, and possibly make some money if enough people buy it).

7) Ad Revenue

I doubt this is going to be enough to retire on, but programming language websites often have the advantage of traffic. Hosting the tool downloads and the documentation can provide an incentive for a lot of repeat visitors. It might not be much, but it's always nice when your hobby is able to buy you a pizza a couple times a year, right?

8) Conferences and speaking engagements

I'm not sure how large a community has to get before speaking engagements would be likely to take up more than a week in any given year. Conferences are probably hit-and-miss in terms of revenue generation. You might end up making a little bit of money, but you could similarly lose a whole bunch.

9) Embedded runtimes/interpreters/compilers

If you could convince a manufacturer of some device (e.g, a mobile phone) to include your implementation of language X, then presumably you could negotiate royalties per-device. I assume that some of the mobile Java implementations provide some sort of financial incentives for their creators?

10) ???

Can anyone else think of ways in which programming language design (or implementation) can be used to generate revenue? Let me know in the comments, because if you have a guaranteed get-rich-quick-scheme, I might have a programming language to sell you :-p

Wednesday 26 August 2009

Lope

I'm working on a programming language that follows the general principles of Bigraphs and bigraphical reactive systems. For simplicity's sake, think term-rewriting with process mobility.

I've written up something that may eventually become documentation for an implementation of this language at:

http://www.expdev.net/lope/

It's still a work in progress, but I would definitely appreciate any thoughts or comments. You can either comment here or email me using the address in the side-bar.

Tuesday 25 August 2009

I laugh at your puny human 'objects'

Let's say that Earth is being invaded by aliens. The last tatters of the US government (and a motley crew of scientists and caravan enthusiasts) are holed up in a secret government base in the desert, where a crashed alien ship is stored. One of the dashing action heroes realises that he can engineer a computer virus to take out the alien shields that are preventing any meaningful counter-attack. Our brave hacker whips up some code, which must be delivered to the alien mothership using the (now-repaired) alien fighter. They sneak into the mothership undetected and upload the virus.

At the moment of truth, as they are about to detonate a nuclear device and make their escape, the virus program throws an exception because the behaviour of the 'AlienMothership' class differed slightly from our hero's interpretation, and the aliens succeed in taking over the world.

OK, so I ripped most of that off from Independence Day, but I think it goes to the heart of my least favourite technology: objects.

I'll freely admit that this is a bit of a rant. You're entitled to disagree.

Objects are a bad model for the universe. There, I said it. Object Oriented Programming (OOP) is oversold as a "natural" way of modelling things. It really isn't. Let's examine why:

Let's start with encapsulation. I have no problem with encapsulation, as such. It's a great idea. Except when it isn't. When you have hidden (mutable) state, I think it's pretty much a terrible idea. You define a nice tidy interface (or class definition, or whatever terminology you prefer), and then call some methods from another location. At any given moment, that object is in some state, and the meaning of calling another method on that object could be completely different. X.a() then X.b() may be completely different to X.b() then X.a(). This implied ordering is not really expressed anywhere. There might be an in-source comment or a note in the documentation that mentions it, but really, you're on your own here.

I'm not talking about incorrect behaviour here either, where it would be possible to check (at runtime) that a call to X.a() never occurs after X.b(). I'm referring to a situation where both execution orders are perfectly valid, but have totally different meanings. How can I resolve this? Well, naturally, I just look inside the class and figure out how internal state is modified and what the behaviour will be depending on the internal state. Whoops! I'm basically back in imperative-land.

To summarise, I think hiding behaviour inside objects makes no sense. "Hiding" computation away is basically ignoring the point of the program. Abstracting away irrelevant computation makes sense, but OOP takes this paradigm way too far, hiding away both irrelevant computation and the computation we are interested in.

I asserted earlier that I thought objects were a poor model for the universe. I'll try to elaborate on this claim.

The classic OO examples always feature things that are somewhat modular in their design, interacting in terms of clearly defined events, with some internal state. For example, one might model a bicycle with wheels and a 'pedal()' method. Or a 'Point' class that perfectly captures the fact that a point has x and y coordinates, with some methods to handle translation or rotation or any other interesting operation.

But a 'point' is just data. Why does it have behaviour? In this case we're basically just using objects to control name spaces. It's nice to be able to have the word 'point' appear in operations on points, and have all of the functionality associated with a point in one place. Great, so let's do that, but instead of hiding the state, let's have a 'Point' module with no internal state, which gathers up all of the point-related functionality that operates on values of type 'point'.

A bike won't do anything without a person to pedal it. A bike makes good sense from an OOP point of view. We can have some internal state, recording things about the bike. It's position and maybe its speed and direction of travel. The "pedal()" and "turnHandleBars()" methods alter this internal state. But a bike exists in the real world. The "world" records the position of the bike, not the bike itself. You can't pick up a bike in the real world and ask it where it is, or where it is going. A real bike stores none of this information, rather the context in which the bike exists tells us all of that information.

So when we model a 'Bike' in an OO context, we're actually talking about a bike in a particular context. The claimed decoupling just hasn't happened. It's unlikely that any natural implementation of a bike could be picked up and re-used in a context where different world-assumptions exist. Perhaps we want to ride a bike on the moon! It seems unlikely we'd be able to do that without going back and changing some internal 'gravity' parameter inside the object. When we model the world this way, we are encoding all sorts of assumptions about the world into the object itself.

If we do the 'right thing' here and remove any world-specific state from the Bike class, what have we got left? In this case, essentially an empty object that simply records the fact that a bike exists. Why do we need an object to do that?

Then there's the question of active and passive behaviour. A bike does not move itself. A person does. A method in the 'Person' class might call the 'pedal' method on the Bike class. This is a relatively sane operation. Calling methods on a Person becomes a much stranger kind of game. Obviously this is a modelling task, so we're abstracting away from the real world, but there is only one kind of method-calling, which models the interaction between a passive system and an active one. Where is the thread of program control? What about active objects calling active objects? Where do 'utility' functions fit in? They have no real-world equivalent, but they still get shoe-horned into the OO paradigm. Don't even mention concurrency in this situation - that's just a horror show waiting to happen.

This isn't just irrational OOP-hatred, by the way. I used to do a lot of programming in Java and C++. These days I use SML. I've found it to be a vast improvement on the situation, and here is why:
  • Records, Tuples and recursive data types fulfil most of the "structured data storage" uses of objects.
  • The module system provides the kind of name-space control and "bundling" for which people use classes.
  • Referential transparency means you can understand easily the meaning and purpose of a given function that operates on data. There is no "hidden state" which modifies this behaviour in unpredictable ways.
  • The "control" of the program follows one predictable path of execution, making mental verification considerably easier.
  • Important computation isn't inadvertently "hidden away". If computation happens, it is because there is a function that does it explicitly.
  • Clear distinction between "passive" data and "active" computation.
  • No hidden state means it is much harder to unintentionally model the object of interest and its context together.
The only thing that object orientation does for most programs is to provide basic name-space control. I don't think it significantly helps maintainability or readability. There are much better ways to do name-space control than wheeling out a giant, unwieldy object system that everything has to be crammed into.

I think the problem essentially exists as a result of static modelling of the universe. If you freeze a moment in time, then sure, everything does look like objects. But we're interested in behaviour and time and computation, none of which are captured very well by bolting on some "behaviour" to an essentially static model of a system. And sadder still, instead of putting the behaviour somewhere sensible, it gets wedged into the static models themselves!

There are a few other things I really dislike. Inheritance, for example. this post is getting really long though, so I'll stop here with the comment: If I was fighting the alien hoards, it wouldn't be with objects.

Friday 21 August 2009

Worrying trends in programming languages: Javascript

Why is Javascript so popular?

It seems that in certain circles, the answer to any question appears to be "Javascript!". With the rise of large social networking platforms and browser-based "desktop-style" applications, it appears that more and more of what we do on a daily basis is likely to be powered by traditionally "web" technologies.

The announcement of Google Chrome OS seems to suggest that at least some people believe that the desktop and the web should no longer be distinct at all. This is totally worthy as a goal, and I like the idea of removing the distinction. However the implications are a bit scary.

Some people (me included) don't really like writing Javascript, but luckily there are several compiler projects that will generate Javascript from your non-Javascript code (Google Web Toolkit springs to mind immediately, though I'm sure there are many others).

Javascript is an odd triumph in programming language terms. It is almost universally available in modern web browsers. It's truly "cross platform" in all the ways that Java really isn't, in that most implementations are reasonably standard across platforms, without the requirement to install a vendor-specific virtual machine or anything like that.

But couldn't we do better? Why on earth would we take a language that can be compiled to efficient native code and then compile it into a slow, interpreted language? We appear to be ignoring almost all of the advances made in programming languages in the last 20 years. By compiling to Javascript, we throw away information that would permit efficient optimisation or static analysis for security. It just seems insane!

The situation is complicated further by the likes of Adobe's Flash and (more recently) Microsoft's Silverlight. With Flash, I am basically instantiating yet another Javascript (well, Actionscript) environment inside my browser. The goals are essentially the same. If it's possible (and even desirable!) to start writing desktop-style applications in Javascript, shouldn't Javascript be able to do almost everything that Flash or Silverlight can? Surely with a little thinking, we could do better.

Well I'm perfectly aware of why Javascript has become as popular as it is, I don't see why it should continue to become more popular. Embedding a virtual machine inside a web browser that would permit execution of some quasi-compiled form of Javascript would be one way. Open up the floodgates and let other languages target the same VM directly. With a bit of JIT compilation, it could probably even be an efficient way to execute some programs, within a browser-based security model. You could even implement a version of the VM in Javascript itself for legacy browsers that don't implement said VM.

But this still appears to be an imperfect solution. Ignoring the problems associated with trying to encourage standardisation or adoption of web technologies, it's still wasteful and just replaces the question "why are we writing desktop applications in Javascript?" with "Why are we running desktop applications inside a web browser?"

The basic technological need that Javascript fulfils very well is the ability to run untrusted code in a standard way, without needing to download or install anything. It provides a standard way to display and interact with an application through the browser, while still allowing nearly limitless customisation.

So putting on our programming language designer hats, what would a Javascript-replacement need to provide?
  1. Security - the ability to run untrusted code in such a way that we need not worry about its source. Similarly, we must be able to control the information it has access to, allowing it certain types of information but at a level far more restrictive than user-level operating system access control would provide.
  2. Zero installation - We may want the illusion of persistence, but we want to be able to access this application from any machine we may sit down at, without worrying about platform installation restrictions or where our data goes.
  3. Uniform display mechanism - HTML still appears to be the best candidate here. We still need to be able to render HTML, but I imagine if we could provide some native components that support hardware acceleration for things like video and 3D applications, we might kill two birds with one stone.
So, in my very armchair-philosophical way, I think that this can all be solved in one easy step:

Download, compile and run anything presented within a web page

That's right! Let's just run it. It would need to be in some sort of bytecode form, but that bytecode would be designed in such a way that it is relatively easy for the browser (or operating system?) to transparently compile it to native code. The application has the full privileges afforded to any other desktop application. It can access and manipulate the DOM in the web browser by any means it wishes. We could presumably provide a list of resources available to the application, so that if we want for it to be able to access an OpenGL or DirectX surface to do fast 3D, or display streaming video, this is fine.

Now, before you write me off as a complete moron, I know, this would probably present some security problems. We might not want to allow unrestricted access to our file system or memory to untrusted programs. This is where I think we need one more addition to our system: Proof-Carrying Code

The basic idea is that the bytecode that is embedded as a resource in a web page comes with a proof. While writing proofs is difficult, checking proofs is computationally inexpensive and relatively simple. The program provides a proof that it is well-behaved with respect to the restrictions we wish to place upon untrusted web-based programs, and our browser can verify that the proof does indeed guarantee that the bytecode is well-behaved. You can think of the proof as a portfolio of evidence for the safety of executing the bytecode - the browser can inspect this evidence (and the bytecode) and establish that the security properties hold itself - we don't need to "trust" the proof at all. As long as this proof-checking succeeds, we can run this program with total confidence in its inability to do anything bad to our system.

However, as I said before, writing proofs is difficult. Except that in this case, our compiler should be able to do it largely automatically. If you write your web-based program in a high-level language that provides no facilities for doing anything bad, then it should be relatively straightforward to automatically construct a proof that will satisfy the browser's proof-checker. The difficulty associated with proving that the program is well-behaved is going to be largely proportional to the low-level constructs you wish to access. It might not be viable to verify certain kinds of programs - I'm not sure, but at least our efforts would be going into figuring out how to construct proofs automatically, rather than figuring out how to force everything we want to do with computers into the limitations of an antiquated scripting language.

Thursday 20 August 2009

A prototype static analysis tool for observable effects

I've had a piece of code kicking around for a while that hasn't really been doing anything, so I've decided to wrap it in a basic web front-end and unleash it upon the unsuspecting public.

It's a tool for performing a very basic kind of specification checking for a simple ML-like language. The idea is that you construct a specification consisting of *traces* of observable effects, and then the compiler can statically determine whether your program behaves according to this specification. It does this by automatically inferring a process algebra-like behavioural type for the program, and then using this as a representation against which to perform specification checking in a tractable way.

An example:

OPERATIONS
insertCoin
button1
button2
takeDrink1
takeDrink2
coinReturnButton
takeCoin

NECESSARY

SAFE
insertCoin,button1,takeDrink1
insertCoin,button2,takeDrink2

FORBIDDEN
insertCoin,_*,insertCoin
The Operations section defines which operations are of interest to us. Naturally our program could be producing any number of observable actions, but we may only be interested in specifying certain types of behaviours. In this case, we're specifying a program that interacts with a vending machine.

Each action (e.g. insertCoin) corresponds to some library call in the language that produces a side-effect. Because the language (which I will describe shortly) is "mostly functional" (in the style of ML), there is no mechanism to introduce new side-effects - they have to come from a built-in library function, or some foreign function interface.

The (empty) Necessary section is the strongest type of specification - it says "the program must be able to behave according to all of these traces, and must not be able to exhibit any other behaviour". When it is empty (as in this example), it has no effect.

The Safe section specifies a weak liveness property, "the program must be able to behave according to at least one of these traces". We have two separate traces defined in our Safe section in this example, each corresponding to a "sensible" interaction between our program and the vending machine. The compiler will halt and issue an error if the program is not able to behave according to any of the traces in a non-empty Safe section.

The final section is the Forbidden traces. These act as a general "pattern match" across all the possible behaviours that a program is able to exhibit. In this case, we specify that we never want our program to be able to insert two coins into the machine. The underscore (_) operator is a wild card, standing for any action that appears in the Operations section. The asterix (*) has the normal meaning one would expect from regular expressions, meaning "zero or more occurrences of this action". So the final trace demands that there never be two occurrences of insertCoin in any of the possible program behaviours.

Now, an implementation!

fun main x = let v = insertCoin () in (if rand_boolean() then ((button1 ());(takeDrink1 ())) else ((button2 ());(takeDrink2 ())))

val _ = main ()
Now this implements our specification. The web-based tool will report "specification satisfied", and will print a visual representation of the behavioural type that it has inferred from the program text.

The tool is at: http://www.expdev.net/tracespec/

I will upload the (as of yet) unpublished paper describing the internals of the system and hopefully some better examples and documentation later tonight. Let me know if you would like to know more.

The tool is pretty fragile at the moment. The error reporting is very bad in most cases. Let me know if you come across any totally weird behaviour, because part of this unleashing-on-the-public exercise is to try to figure out what is and isn't working, and how I can improve it, so I would appreciate any feedback.

The idea (before you ask) is the encourage a very light weight form of specification. There is no execution going on here. It is supposed to mimic the function of certain types of unit tests in a completely static way. The way it is implemented at the moment is a rough prototype. Once I have proved to myself that this is a feasible kind of static analysis to perform, I may work on integrating it into a compiler for a general-purpose language. There is no particular restriction on the source language, however it is most likely to be feasible for a strongly typed functional language.

Tuesday 18 August 2009

Hardware/Software Co-design

I'll preface this post by saying: I don't know much about hardware.

I have, however, spent a lot of time around hardware engineers. As a very naive programmer, I generally assumed that what they did was programming with some "extra bits" added, though I've long since been corrected.

Hardware is fast

How fast? For FPGA developments, I believe many applications can be 200 times faster. I believe even a reasonably inexperienced hardware designer can achieve speed ups of 50-100 times on many applications. It's also worth thinking about power consumption. The power consumption of an FPGA can often be a small fraction of the equivalent processing power required to hit the same performance constraints using commercially-available microprocessors.

This all sounds wonderful. Why aren't we all doing this? Well, for me, the problem is basically me.

I have neither the tools, nor the experience, to design non-trivial solutions to problems in hardware. If I were to sit down and try to solve a problem in hardware, I would probably end up writing VHDL or Verilog in much the same way that I would write C or Java, which would result in really, really awful hardware, which would be unlikely to be efficient. The maximum clock-rate would be very low, and finding a device big enough to fit my resulting hardware on could become an expensive undertaking.

That said, I still really like the idea of using hardware to solve problems. While specialist hardware engineers will always have the job of designing high-performance hardware with tight performance constraints, is there any low-hanging fruit which we (as programmers) could target for using reconfigurable logic devices as part of our programs?

The most obvious way of achieving this seems to be with the general idea of "hardware acceleration", where a special-purpose device (such as a PCI-X card with an ASIC or FPGA implementation of some algorithm) takes over some of the hard work from the CPU. The device manufacturer provides some sort of software library that hides the hardware interaction behind nice high-level function calls that are familiar territory for programmers.

These are great for specific applications, but I'm not aware of any "general purpose" cards that would permit programmers to integrate them into an arbitrary application without having some knowledge of hardware design.

Perhaps the next obvious alternative is compiling software into hardware. This is dangerous territory. There have been so many claims of software-to-hardware compilers that I won't even bother to list them. I'm sure you can find hundreds with a quick Google search. The problem with most of these is that they are actually just hardware semantics hidden underneath a veneer of some mainstream programming language. A programmer familiar with the source language will still not be able to produce efficient hardware without knowing something about hardware.

I think there could be two possible solutions, which I will sketch here:

Component-based Approach

Presumably we could get experienced hardware engineers to implement a wide variety of software-style components as efficient hardware. We use the same approach as the domain-specific hardware accelerator manufacturers, hiding the complexity of hardware interaction behind some nice software libraries. If you had a significant portion of the expensive operations from a programming language's standard library available as hardware components, it wouldn't take a particularly smart compiler to replace certain standard library calls with calls to the (functionally identical) hardware-wrapper library.

But there are some problems that I can see.

It is unlikely to be efficient in terms of communication, area or power consumption to simply push a whole lot of small, infrequently-used library calls into hardware. There would need to be a lot of static (or runtime profiling?) analysis to determine where there are efficiencies to be gained. The compiler would be forced to "schedule" components into the finite area available on the FPGA. This would have implications for latency and throughput. It might be necessary to buffer large numbers of calls before executing them. The performance gains from doing operations in hardware are likely to be eaten up by the communication overhead resulting from having to move data from registers in the CPU (or from processor cache, or from main memory) to the FPGA. Similarly in a traditional imperative setting, this is going to be an interruption of program control. The program will have to stop and wait for the results from the FPGA. The alternative is concurrency, but as I've previously said, concurrency is hard, and this is the type of heterogeneous task-level parallelism that is really hard.

So it appears that this approach would require putting a lot of smarts into the compiler. We would need good performance heuristics, something resembling auto-vectorisation and automatic parallelisation, and likely an ability to trade-off latency for throughput.

It all seems a little bit challenging, given the state of the art of each of those areas. It would appear that some of the purely functional languages would be best-suited to this kind of approach, but even in the absence of side-effects it seems uh... difficult, at best.

Language-based Approach

So if we're not going to expect the compiler to perform a rather sophisticated brand of super-compilation on our programs, can we instead structure our programs (and programming languages) to make this kind of hardware/software co-design easier?

I believe that this is one of the possible future directions for the JStar project, although I'm not aware of the technical details in this case. The data-structure-free approach may permit the kinds of analyses required to allow for efficient scheduling of components onto an external FPGA, so it definitely seems like an interesting avenue to keep an eye on.

Another avenue has to be concurrent (and functional?) languages. These are designed to express concurrent computation, which is essentially what we are trying to maximize, while minimising the presence of mutable state. With mutable state largely out of the way, you are free to have copies of data lying around. There are still questions as to how we maximise the efficiency (and indeed, even approach predicting the efficiency).

I'm aware of efforts to compile Esterel to hardware, though I have no idea to what degree this is practical or whether it is used in industry.

It strikes me that a model-based approach to software development could be used to make the entire process a lot less painful. By starting with a high-level model, it would be possible to refine towards both hardware and software implementations of different parts of the system. Provided you could contrive acceptable heuristics for predicting performance, it seems like you could start to play this sort of game:

I have a high-level abstract specification S.

I have a set of (hardware) components:

H = {h1,h2,h3}

I have some software components that are synthesised from S, or are user-supplied:

W = {w1,w2,w3}

We want to choose a subset X ⊆ H and Y ⊆ W, such that:

S ⊑ x1 || ... || xn || y1 || ... || yn

Where '⊑' is some appropriate notion of refinement and '||' is parallel composition. I'm not sure if this is more tractable than simply solving the problem outright for a given language, but it certainly seems like it would be considerably easier to verify the correctness of the decomposition of the program into software and hardware components, which would seem rather more difficult in this case than for a traditional compiler.

Is anyone aware of any projects that attempt this kind of thing? I'd be interested to hear from hardware and software people alike about their opinions on enabling programmers with no specialist hardware knowledge to use hardware in a manner that is both efficient and reasonably familiar.

Monday 17 August 2009

Housekeeping

I'm working on another post, but I thought I would briefly mention two things:

1) I have turned on Google AdSense for this blog. Let me know if the ads are particularly irritating. I mostly turned it on for my own personal curiosity, rather than because I'm hoping to quit my day job using the ad revenue.

2) I'm on Twitter - http://www.twitter.com/gianp - I've actually had an account for a long time, but I'm actively using it now.

Sunday 16 August 2009

Simple patterns for better arguments about programming languages

I somehow get myself into a lot of arguments about programming languages. Perhaps it's because I talk about them a lot, and everybody has an opinion!

Getting into arguments about programming languages generally means listening to a large number of value-based judgements until somebody gets bored and admits that language X really isn't as bad as he or she originally asserted, and yes, maybe language Y does have some flaws. This is largely counter-productive. If we're going to argue about the best way to skin a cat*, let's argue about things we can actually compare. So I present in this post a number of more objective ways of talking about the merits of programming languages such that you might actually persuade somebody that your well-informed opinion is actually valid!

(* Please don't, that's cruel and horrible)

I often hear the word "powerful" used to describe the relevant merits of programming languages, as in "People use Ruby because it is more powerful". This is often used in conjunction with lots of other words like "maintainable", "simple", "faster", "easier" etc etc. These are all largely intangible qualities that could just as well be described by "I prefer language X".

That said, maybe there is some value in comparing languages. So what can and can't we measure?

It's worth creating a distinction at this point between the programming language itself (i.e. syntax and semantics - the set of valid programs), and the eco-system that exists around the language, in terms of compilers, tools, libraries, user-bases etc. Sometimes these overlap in a big way, especially in cases where there exists only a single implementation of a given language.

Comparison 1: Performance

We have some reasonably good metrics for "performance" of a given implementation for a certain application. These are often pulled out when one party in a heated discussion about the merits of a programming language demands evidence to support claims of superiority or inferiority. That said, as a metric for comparing languages, they are pretty lousy. Sure, it's interesting that you can write a compiler for some language X that outperforms a compiler for language Y for a certain application. Big deal. It might say something about the ability for the program to express efficient solutions to problems, or it might just tell you that one compiler is better than another.

Before I wave my hands and dismiss "performance" as a useful metric altogether, it is true that some languages lend themselves to efficient implementations better than others. The Computer Language Shootout Game makes for interesting reading, even if it is not a completely scientific means of comparing whole languages. Without beating up on anyone's favourite languages, languages that permit dynamic behaviour (usually requiring interpretation rather than compilation-proper) don't really lend themselves to static analysis and optimisation. Sure, it happens, but it is added to the runtime cost of the application (because it is done, by necessity, at runtime). I don't think anybody would really have a problem admitting that languages like PHP, Python, Perl and Ruby are unlikely to be considered in the same performance category as C/C++, ML, Fortran and a bunch of other languages that do lend themselves to good compile-time optimisation and compilation to fast, native code (or something with comparable performance).

So, take-home talking point number one: Language X lends itself to compile-time optimisation and efficient code-generation that is better than language Y's.

You need to be careful with this one though - just because people haven't written good optimising compilers for a language doesn't mean it's not possible or even difficult! Sometimes it's just not a priority. If you're going to use this talking point, you need to be able to substantiate it! Think about things like: presence (or absence) of very dynamic features, referential transparency, treatment of constants, and syntactic ambiguity resolvable only at runtime (Perl, I'm looking at you).

Comparison 2: Readability

This is argument is abused regularly. Arguments about readability often boil down to "Language X is different to language Y, which I am used to, therefore I find it harder to read!". This is not a good argument. You're basically just saying "I find it easier to use things that I am familiar with", which is uh, pretty obvious, really. Some other person who uses X more than Y probably finds Y equally unreadable.

There might be one tiny point for comparison here, although I would hesitate to use it unless you're very sure that you're correct. It basically goes like this:

How much information about the expected run-time behaviour of a program can I discern from the structure of a small piece of the program?

To elaborate, what is the smallestt piece of the program that I can look at independent of the rest while still having at least some idea what it is meant to do? Can I look at just one line? A few lines? A page of code? The entire program spread over multiple files? This is probably equivalent to some kind of modularity property, although I don't mean this in terms of objects or module systems. I mean, "if something is true within this piece of code now, will it still be true no matter what else I add to the system?"

I figure this corresponds to "the amount of things you need to keep in your head" in order to read code. Smaller is probably better.

Talking point two: Language X requires the programmer to mentally store fewer things in order to read and understand the program than language Y.

You'll need to be able to substantiate this if you're going to use it. Think about things like scoping rules, syntactically significant names and consistency. Does this operator always mean the same thing? No? Does its meaning vary in some consistent way that is indicated by a (relatively small) context? It doesn't? Oh dear.

Comparison 3: Bugs!

Don't get drawn into this one lightly. Discussions about bugs can go on for days. The sources of bugs, the causes of bugs, and what language design decisions influence the ability to detect (and indeed prevent) bugs.

Being a formal methods geek, I'm pretty passionate about this point. I think bugs in all their forms are bad things. Some people see them as an unavoidable side-effect of producing software, much like mopping a floor will make the floor all wet.

I think a well-designed language should allow a compiler to prevent you from making dumb mistakes. I'm going to beat up on PHP here, because really, anybody who has used PHP pretty much loathes it. My pet peeve:


$someVeryComplicatedVariableName = doSomeStuff();

print $someVeryComplicatedName;

Whoops! I guess I didn't type that variable name correctly the second time. Oh well, don't worry, PHP's default behaviour is to initialise it to an empty value that is coerced to an appropriate type for the context. In this case, my program would print nothing at all. Sure, it issues a notice somewhere, but this isn't considered an error in PHP, because we don't declare things! In this case, the design of the language prevents the compiler/intepreter from stopping us from doing something very dumb.

Languages that lend themselves to compilers that enforce global consistency in some way are good at preventing errors. I've already said in a previous post that I'm a fan of type systems that prevent dumb mistakes. Obviously in a programming language there is always some conceptual gap between what we expect the compiler to do, and what it actually does. To me a well-designed programming language is one that will prevent me from being inconsistent, and which will tell me if my understanding of a program differs significantly from the compiler's interpretation of it (manifested in the way I am writing my program, probably as a type error!).

Finally, how many things are put in front of me that I have to get right in order for my program to be correct? Oh, I have to do my own memory management? So it would be bad if I got that wrong, right?

Talking point: Language X is designed in such a way that a compiler or interpreter can detect and report a larger class of errors, and prevent more simple mistakes than one for language Y.

Do your research on this one too. Unfortunately there are very few studies with substantial findings on the types of errors that programmers make. You'll need to restrict yourself to tangible classes of errors that are detectable in language X, but will not be detectable in language Y, by virtue of the design of the language. Remember, a bad compiler might not report errors, but that doesn't necessarily mean it's impossible to detect them!

The natural counter to argument is usually to propose an absurdly complicated way by which it might be possible to simulate the language-based features of language X in language Y at the application level. For example, "We'll search-and-replace to replace every occurence of variable x with a function that validates its internal structure!" At this point, you should probably just sigh and walk away, safe in the knowledge that you don't need to worry about any such absurd solutions in your own daily life.

Comparison 4: Eco-System Factors

If you want to argue about libraries and user communities, be my guest. If you're having an argument about programming languages, these things are probably important, but they really only tell us the way things are, not why they are like that or how they should be. Arguing about how things should be is not particularly helpful, but similarly, "Everyone uses X so it must be better than Y" is a very unhelpful argument. A lot of people get cancer, too. Doesn't mean I'm lining up for it.

Talking point: Language X has considerably more library support for than language Y, and that is what I am interested in doing.

Perfectly valid. Just don't fall into the trap of suggesting that having more libraries means that one language is better than any other. Most languages worth their salt actually provide some sort of foreign function interface, so the idea of a library being completely unavailable in a language is pretty rare. You might have to put a bit of work into it, but it's certainly not a limitation of the language just because someone wrote a library for X and not for Y.

Comparison 5: Non-comparisons

This is my "please avoid" list. If you use any of these arguments in a discussion on programming languages, you should really look at what evidence you have, because you probably don't have any:

  • Lines of Code - please, please avoid using this. It's just not relevant. If you use this, you have reduced an argument about the relative merits of programming languages to one about typing speed.
  • Elegance - I know what you mean, some solutions are elegant, but this really can't be quantified. It's probably the solution that is elegant, rather than the solution in a given language. It could probably be expressed elegantly in almost any language by a programmer sufficiently familiar with the conventions of that language.
  • "I don't need a language-based solution for that, we have social conventions". No, no, no. What you're saying here is that you are accepting that this problem is still a problem if people don't follow the conventions. Guess what? People are really bad at following rules. Some people are just born rule-breakers.
  • "Language X is too restrictive". Really? I find those pesky laws about not going on murderous rampages rather restrictive too. If you can't qualify this statement with a very specific example of something that is both within the domain of the language, and which genuinely can't be done using the features of the language in question, then you're just saying "Language X doesn't let me do things exactly how I did them in language Y".
So I hope this all provides some food for thought. I would love to hear of any other arguments that people resort to about programming languages that really annoy you. Or perhaps I've missed some genuinely valuable comparisons that can be made?