Tuesday, June

27th,

2023

Having been a programmer for a long time now, I have experienced my

fair share of programming languages. What strikes me the most is that

programming languages have not improved much over the years. Java,

for example, has certainly improved from when I started using it in

the mid-nineties — but only in pretty minor ways. We still get

buffer overflows and integer overflows. The compiler still cannot

tell when our loops will terminate (yes, this is possible). Aliasing

is still a complete unbridled mess. Even Rust, my favourite language

du jour, only offers a minor improvement on the status quo. These are

not stop-the-world everything has changed kinds of improvements.

Still, big improvements are possible. I now use, on a daily basis, a

language (Dafny) which often

genuinely amazes me. I’ll admit, its not super easy to use and

perhaps not ready yet for mainstream — but, it gives a glimpse of

what is possible. Dafny’s ability to statically check critical

properties of your program goes well beyond what mainstream languages

can do (that includes you, Rust). Here’s a simple example:

```
function Gcd(a:nat, b:nat) : (g:nat,x:int,y:int))
// Bezout's identity
ensures (a*x)+(b*y) == g
{
if a == 0 then (b,0,1)
else
var (g,x,y) := Gcd(b%a,a);
(g,y-((b/a)*x),x)
}
```

This is a recursive implementation of Euclid’s extended GCD

algorithm

(i.e. an integral part of modern cryptography, including

RSA and

ECC).

Using the `ensures`

clause I’ve specified a

postcondition — that

is, a property that should always hold of the return value. This

particular postcondition corresponds to Bézout’s

identity.

That is, *a theorem about numbers proved by Étienne Bézout in the 18th
century*. The amazing thing is that, in order to check my program is

correct, Dafny has reproved this theorem for me.

## Bits and Bytes

The above example was taken from our DafnyEVM

codebase.

Here’s another

example

which is, perhaps, more concrete:

`function ToBytes(v:nat) : (r:seq`)
ensures |r| > 0 {
// Extract the byte
var byte : u8 := (v % 256) as u8;
// Determine what's left
var w : nat := v/256;
if w == 0 then [byte]
else
ToBytes(w) + [byte]
}

The above is a straightforward (recursive) function for converting an

arbitrary-sized unsigned integer (`nat`

) into a sequence of one or

more bytes (following a big endian representation). Here, `ToBytes()`

has an `ensures`

clause clarifying it always returns a non-empty

sequence. *Dafny checks at compile time that this is always true*.

Now, here is a function taking us in the opposite direction:

`function FromBytes(bytes:seq`) : (r:nat) {
if |bytes| == 0 then 0
else
var last := |bytes| - 1;
var byte := bytes[last] as nat;
var msw := FromBytes(bytes[..last]);
(msw * 256) + byte
}

There isn’t anything too special going on here (yet). But, now the

magic begins! What we want to know is that these two functions are

“opposites” of each other. We can do this like so:

```
lemma LemmaFromToBytes(v: nat)
ensures FromBytes(ToBytes(v)) == v {
// Dafny does all the work!
}
```

This might not seem like much, but it represents something you cannot

easily do in other languages. This `lemma`

asks Dafny to check that,

for any possible `nat`

value `v`

, it always holds that

`FromBytes(ToBytes(v)) == v`

. *Again, Dafny checks this at compile
time — no testing required!*

Finally, an interesting puzzle remains. For an arbitrary sequence

`bs`

of bytes, does `ToBytes(FromBytes(bs)) == bs`

always hold?

Again, Dafny can answer this for us almost immediately. If

you’re interested to know the answer, take a look at the lemma we

came up

with.