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 was dated June 7th 2010.

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:

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:

• RFC#23 (Templates). This added support for type polymorphism allowing us to use types such as vector<T> (i.e. as in C++ templates or Java generics). This is a fairly fundamental feature which enabled significant improvements to the standard library (see e.g. std::collections::vector).

• RFC#58 (import with). This extended the syntax for import statements to support a with clause. For example:

  import std::vector with Vector
  

• RFC#64 (for each). This finally added a syntax for for-loops to the language which had been sorely missing! For example:

  for i in 0..|arr|:
     m = m + arr[i]
  

• RFC#66 (type inference). This added support for bidirectional type inference allowed type information to flow both up and down the AST for an expression. Amongst other things, this allows us to omit type parameters in most cases. For example:

  // Create empty vector
  Vector<int> vec = Vector()
  // Add something to vector
  vec = push(vec,1)
  

  In the last line, without type inference, we’d have to give the type parameters explicitly (e.g. push<int>(vec,1)). Type inference also helps implementing native types (e.g. a string literal assigned to a JavaScript string can be implemented directly as such).

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:

• (Teaching) Whiley has been used for teaching here at Victoria University since 2014, and also at other instituations as well. For example, at Stellenbosch University under Prof. Bruce Watson and Macquarie University under Dr. Matt Roberts. It was also used for a summer school on Formal Methods in China.

• (Experimental Platforms). There have been a bunch of experimental projects trying to get Whiley working on different platforms, including WebAssembley, an FPGA, the Crazyflie Quad Copter, the Ethereum Virtual Machine and more! Whilst these have all been instructive in the design of Whiley, perhaps the most promising future target is WebAssembly.

• (Functional Reactive Programming). The Web.wy provides a general platform for React-style Functional Reactive Programming (i.e. including a virtual DOM). Whilst this remains at an early stage, you can find a simple example here.