Dr. David J. Pearce

Whiley is Ten Years Old!


The first commit recorded in the WhileyCompiler repository on Github is dated June 25th, 2010. That means Whiley has been going for just over ten years already! Wow, time sure does fly. It’s not a very interesting first commit though. And, looking closely, you can see that commit is actually from the subversion repository that Whiley was originally hosted in. The first real commit to the GitHub repository is dated November 22, 2010. Again, it’s not a very interesting commit! Since those early commits, a lot has happened — including around 7.6K more commits. The first post on whiley.org is dated June 7th 2010, with the first talking about Whiley coming on the same day.

Anyway, I’m not going to bore you with a full break down of everything that’s happened since then! Instead, here are a few highlights for me right now:

Actual Code

There are now a few projects in Whiley which demonstrate its potential for building useful programs. For now, these are currently mostly restricted to simple web applications:

Game of Life Screenshot
(Game of Life)
Minesweeper Screenshot
(Minesweeper)
Asteroids Screenshot
(Asteroids)

On top of this, a number of libraries have been written which are finding use in various ways (e.g. STD.wy, JS.wy, DOM.wy, Web.wy, Ace.wy, LZ.wy). There is even a simple online package repository!

Request For Comments (RFCs)

The RFC process for developing extensions to the Whiley language has been running since around 2017. At the time of writing, there are 30 RFCs of which around 15 have been completed. A few of the “big ones” are:

In addition to the formal RFC submissions, there are also a bunch of lightweight ideas being floated around as well which may eventually be written up into RFCs.

QuickCheck

Whilst the static verifier that comes with Whiley has slowly improved over the years, it remains difficult to use on large projects. A surprising success has been the QuickCheck for Whiley originally developed by Janice Chin. The essential idea behind this tool arose from the original QuickCheck for Haskell tool developed by John Hughes and Koen Claessen. Essentially, this tool tests Whiley programs by generating inputs automatically based on certain (configurable) criteria, such as only -3..3 for integers, restricting arrays to max length 3, etc. For example, consider this (broken) function:

function find(int[] xs, int x) -> (int r)
// Return cannot be negative!
ensures r >= 0:
    for i in 0..|xs|:
       if xs[i] == x:
          return i  // match
    return -1       // no match

This function is broken because its postcondition doesn’t permit negative values to be returned. Running this through QuickCheck quickly generates the following:

main.whiley:6: postcondition not satisfied
--> main::find([],0)
    return -1       // no match
    ^^^^^^^^^
Stack Trace:
--> main::find([],0)

The great thing about this is that it shows the exact input values which generated the error! And, what’s even better, is that we can run QuickCheck as part of our CI pipeline as well!

Other

Whilst there are too many other things to mention, here are a few more highlights chosen at random:


Follow the discussion on Twitter or Reddit