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:
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:
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
importstatements to support a
withclause. 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.
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.
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!
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.
Follow the discussion on Twitter or Reddit