Today we're going to be doing something a little bit different. And it's
something that brings together many ideas in computer science - and it's
the idea of program correctness. So what we're going
to be thinking about, is what does it actually mean
for a program to be correct, and then how can we specify and verify
that in some kind of precise way. So that's what we're going to
be thinking about today, program correctness.
We're going to come at this problem by means of an example, and the example that
we're going to look at is a simple compiler.
So what a compiler does in computing is it's a program that takes a high-level
language, and translates it down to a low-level language,
which is more easy for a machine like this one to execute.
So what I'm going to show you, is a little Haskell file which I've written.
But it doesn't matter if you don't know anything about Haskell, because it's
really incidental to everything that we're going to talk about today.
It just allows me to do everything in quite a concise way, but actually you can
do everything in any old programming language that you like. But I'm going to
explain everything as we go along anyway. We have two data
type declarations, and we have three function declarations,
or function definitions rather. And what we're going to do, is we're
going to explain what these do by means of some simple examples.
And then we're going to think, well what does it actually mean for the compiler, which
is embedded in this code, to actually be correct? So what we're
going to start off looking at is the source language for the compiler.
And it's going to be a very simple language, it's going to be
the language of integer values combined using an
addition operator. So we're going to be building up simple arithmetic
expressions -- things like two, plus three, plus four.
So here is the data type declaration for this in Haskell. And it's got a few
components, so we'll work through these. So we're declaring a new data type
called Expr for these simple arithmetic expressions, and then the data
type has two constructors for building expressions -- it's got a value constructor,
which takes an integer parameter, and it's got an add constructor,
which takes two sub-expressions as arguments. So this is how we're going to
build up our simple expressions, and they are really
expression trees. And you might be thinking, well what does
"deriving show" mean here? Well, this is a little bit of Haskell magic,
and it just instructs the system to be able to print these things
on the screen, so we can view them. So not everyone's familiar with Haskell, so I'm
going to give you three little examples of values in this
expression data type. And these are going to be running examples
that we're going to be using throughout the video today. So the first one
is going to be e1, and it's just going to be a simple
integer value. So we have an integer here, one,
and then we tag it with the Val constructor, and then we've called it e1,
so we don't need to type this in again. Whenever we type e1 now, it just stands
for Val of one. Our second example is going
to be an addition. So we're going to do Add of Val 2 and Val 3.
So this is like how we would represent two plus three
as a value in our simple expression data type. So we've got a number of components
here - we've got the value two, and we've got
the value three, and then we combine them with the Add
constructor. So it's a little bit more verbose than what you'd normally write
down in mathematics - you'd normally just write down 2+3, but here
we're doing in a programming language, so we need to be a little bit more
verbose, and we're using the two constructors of the expression data type.
So just as one final example, let's do something a bit more
sophisticated, let's reuse e2 and add that onto Val 4. So we
defined e3 here to be the sum of e2 and the value four. So what
this really is is it's two, plus three, plus four. And we
can use the little pretty printer here, which we got from writing "deriving show",
and if we print out the value of e3, what you get is
you get the addition of two and three here as the first parameter to the add,
and then as the second parameter, you have Val 4. So these are three
little running examples of arithmetic expressions
which we're going to put into our compiler as source expressions.
So the next thing we're going to think about is what do expressions in this
language actually mean? And this is very simple in
this case - expressions just denote simple integer values. So we can
think about evaluating an expression. So let's look at the three
examples. So we had e1, and if we evaluated e1, we just get rid
of the Val constructor and we get the value one - very simple.
If we look at our second example, which was two plus three,
if we evaluate two plus three, then of course we're just going to get five. And
if we look at our third example, this is two plus, three, plus four - bit
more verbose - but when we evaluate this one,
we're going to get the value nine, as we expect.
So let's have a look at the source file now, and think how do we actually
define this evaluation function? And it's actually just a very simple
two-line recursive definition. So let's look at the two lines one by one.
So the first line says, if we evaluate a value n,
we simply remove the Val constructor, and we get the underlying value n.
The second line says if we evaluate an addition
of two expressions x and y, all we're going to do is evaluate the first
expression x, evaluate the second expression y -- that
will give us two integers -- and then we can add them together,
and that will be the evaluation of the integer. So it's a very
simple two-line recursive definition. The next thing we're going to look at now
is the actual compiler for these simple arithmetic expressions.
And what it's going to do, is compile from expressions down to
code. And the code is going to be a sequence of operations for a very simple
stack machine. And the stack is just like having a stack of books,
it grows and shrinks, and you always put new values on top of the stack.
So let's have some examples to see how the compiler works first.
And then we'll see how it's actually defined in the code.
If we think about our first example, Val 1, we can compile that one,
and what we're going to get is just a sequence of a single
operation for the little machine. And what the operation is going to do
is just push that value one onto the stack.
If we look at our second example, we had add of two
and three. If we compile that, then we really start to see
what the compiler is doing. It's compiled it down to a lower-level sequence of
operations, and in this case what we're going to do
is we're going to do a single push of the value two,
another push of the value three - so that we have two values sitting on the stack -
and then you'll perform an addition on those two values, and that will leave the
value five sitting on top of the stack. So you start
to see how the compiler here is taking high-level arithmetic expressions, and
compiling them down to lower-level sequences of operations,
which a machine like this one could more easily execute.
So let's have one more example. Let's look at our third example, two plus three
plus four. If we compile this one, then we get
five operations this time. We have push of two,
push of three, and then add. And that will leave the value five sitting on the
stack. And then we push the value four. And then we
perform an addition, and that will leave the value nine sitting
on the stack at the end. So that's what the compiler does.
Let's have a look to see how it's actually defined.
And again, it's just defined as a simple two-line recursive
definition. So if we look at the base case for the recursion,
what it's saying is if you compile a value, this is very simple,
you just simply emit a single instruction, or a single operation,
which pushes the value n onto the stack. Whereas if you compile an addition,
then you have three things to do. What you're going to do is you're going to
compile the first part of the addition, compile
the second part of the addition, and then put an add operation on at the end.
And the ++ here is just a way in Haskell
of combining lists together - it's list concatenation, or list append.
And this then brings us to our second data type declaration at the top.
We're defining the data type for operations, and this is very simple -
there's no recursion involved this time around -
it's just simply you push an integer value onto the stack,
or you can perform an add on the top two values on the stack.
And again we're using the Haskell magic here to derive
a pretty-printer which can print these things on the screen.
So that's the compiler for arithmetic expressions.
But we're not quite done yet, we still need to think about how does
code for this little stack machine actually get executed?
So again, let me give you some examples of this, and then we'll see
how this is actually implemented in terms of Haskell code.
So if we take some examples here. So the first example is just going to be if we
execute the result of pushing one onto the stack,
and we give it the empty stack, then you just get exactly what you
expect - you get the value one sitting on the stack. Remember, a stack is like a
pile of books, and in this case it's a pile of integer
values, and you always put things on the top.
So in this case we're just taking an empty pile, and then putting the value
one on the top. Let's take another example.
Suppose we did push two, push three, and then add, and we
executed that with an empty stack. Then we get the final stack with the
value five on it. So the way this will actually get executed
is the value two will go on the stack, then the value three,
then you'll add them together, and you'll get the value five sitting on top of the
stack. And that's exactly what we get sitting here. So the very last example,
if we did the two plus three plus four example.
So I do push two, push three, perform an addition,
push four, perform another addition, and then hopefully we get the right
result - which we do - which is the value nine sitting on the stack. So this kind of
shows you how the little stack machine actually works.
So let's have a look at the code for this. So the code
looks a bit more complicated, but it's actually completely straightforward, and
we can just kind of talk through this. So the way if we want to execute a push,
and then we have some more code afterwards, in the context of a given
stack, is we're simply going to put that number
on top of the stack, and then continue executing the
remaining code. So very simple - if you want to execute a push,
you put that number on top of the stack, and then you just continue with whatever
it was you were going to continue with.
The second case says, if we're trying to execute an addition,
all we're going to do is inspect the top of the stack, and hope
that we have at least two values, m and n, on top of the stack, and s is
everything else, and all we're going to do is add
together those two values, and then put them on top of the stack,
and then we'll continue by executing everything else that we're going to
execute. So again, very simple. If you perform an addition, you take the
top two values of the stack, add them together, and put the result
back on. That's all that's going on here. And the very last case is kind of the
catch-all case. It says, if you've got any other
code sequence, and any old stack, then there's nothing to do -
you just return the stack. So this brings us now to the issue of compiler
correctness. So what we've defined now, is we've
defined a syntax for our source language, which is simple arithmetic expressions.
We've defined our target language, which is stack machine code, for a simple
stack-based machine. And then we had a compiler, which
translates arithmetic expressions down to the simple stack machine code.
But how do we know the compiler actually does the right thing? That's the point of
this video today, we're thinking about program correctness.
How do we know that our program for compilation actually does the right thing?
So that's what we're going to think about now.
So let's look at our most complicated example,
which was 2+3+4. So there's a bunch of things we could do with this.
We could evaluate it, and we get the result nine - very simple.
We could also compile it. So we could translate it down to some
stack machine code. And then we get push two,
push three, add, push four, and add. And then we could execute that stack machine code
now. So what we could do, is we could execute
the result of compiling that expression, using an empty stack.
And what we get is the value nine sitting on the stack.
Which is exactly what we expect. And you can see here by looking at these
examples, the essence of what it means for this compiler to be correct,
is that when we compile an expression, and then execute the resulting code,
we get basically the same value as when we evaluate it.
So in each case we get the value nine. In the evaluation case we just get the
integer just sitting there on its own. Whereas in
the compilation case, we get a stack with the value nine sitting
on it. So this is the essence of what it means for the compiler to be correct.
If we compile, and then execute the code, it's the same as just evaluating the
original expression. So what we can do now is actually think
about making this precise, and kind of precisely specifying what it
means for the compiler to be correct. And then we can wrap things up by
thinking how can we actually verify that? So what I'm going to do
is write down a simple function definition, which captures
what I've just said about the compiler being correct. So I'm defining a little
function called correct, and it's going to take an arithmetic
expression e as input. And what we're going to do is
we're going to execute the result of compiling that expression,
with an empty stack. And what we want is that that's the same
as the stack we get by just putting the value of that
expression into a stack on its own. So this generalises what we just had.
What this is saying is if you compile an expression e, and
then you execute the resulting code, using an initial stack which is empty,
then what you expect to get is just the value of the expression
sitting as a single little value on the stack. The double equal symbol here
is just Haskell's operator for checking whether two lists are actually equal.
So this captures in a very precise, concise mathematical
way what it means for this compiler to be correct. But how can we
actually check that this property is actually true?
Well, if you were eagle-eyed, you might have noticed right at the top
of my file, I was importing the QuickCheck library.
And QuickCheck is a random testing tool, which Computerphile's already done a very
nice video on with John Hughes, which you might want to check out.
And what QuickCheck does, is it blasts random test cases
through properties. And it tries to check that the property is true
for all of these test cases. So we have a property here - we've got a simple
compiler correctness property. So what I can do then, I can just write
QuickCheck the correctness property, and it will run
100 test cases through it. It will start with very small things like just simple
values like 0, 1 and 2, and so on. And then it will consider larger and larger
expressions, with more and more additions. And it's trying
to find an example which breaks this compiler correctness
property. But it doesn't do it because the compiler is correct.
Maybe it was a fluke? Maybe we can try again - let's try two or three different
runs. And in fact it doesn't matter how many
runs we do of this, this is always going to work. Because the compiler
is actually correct. So, suppose we'd messed up - suppose we had
a compiler, which we'd implemented incorrectly. So let me break the compiler
now. Let me change the compiler, and this is a
very easy mistake to make. Rather than compiling an addition by
compiling the first thing, and then the second thing, and then omitting an add
operation, what I'm going to do is put the add
operation in the middle. And this is a kind of very common mistake - if you teach
compilers to students, this is a very common mistake that you see
in their code. But it will break the compiler correctness property.
So this compiler is now incorrect - let me QuickCheck it. And it's managed to find
a counter example. And in fact any addition
will break this compiler, if you work through the details. What we've seen here
now is how, in a very simple way, you can
capture the correctness property of a small, but interesting program
- a simple compiler - and then how you can actually verify
this, or give high confidence that this is actually doing the right thing,
using an automatic testing tool such as the QuickCheck system.
If you wanted to do this properly, of course you could do some kind of
mathematical proof that it's also correct - or that it's
correct - using some kind of induction. Or if you wanted some machine assistance,
you could maybe use an automated theorem prover, or an automated
proof assistant. But actually, for many applications, just
doing this kind of high confidence activity
of using a random testing tool like QuickCheck, actually gives you
very strong confidence that your programs are actually correct.
But ultimately, the gold standard is always to do a proper
inductive proof, or to use some kind of proof assistant to do it for you. So
just to summarise what we've done today, we've been looking at the problem of
program correctness. And what we've shown is how you can
prove a simple compiler correct. And the way we came at this, is we first
of all defined what the source language for the compiler was,
which was simple arithmetic expressions. Then we defined
what the target language was for the compiler, which is simple stack machine
code. We defined a semantics for both of those
languages - we worked out a way of evaluating
expressions, and executing code - and then we had a compiler which
translated from one into the other. And then finally, we formulated this
simple correctness property, and used the QuickCheck system to check
that it was correct with high confidence. And of course if you want to do this
properly, you could do a mathematical proof,
using some form of induction, or you could even use some kind of mechanised
proof assistant. And maybe those would be interesting topics for other Computerphiles
another day. So that's it for today - see you again next time!