Looking Forward to 2015

It’s scary to think that 2014 has been and gone, and that I still haven’t released the next major version of Whiley!  Despite this, I have been busy improving the compiler and language and I thought it would be helpful for me to recap what was achieved last year, and what the goals going forward are.

Recapping 2014

So, what happened with Whiley in 2014?  Well, there were 10 minor releases starting with v0.3.22 in Feb and roughly 110 issues were closed.  The main highlights being:

• Changes to Syntax.  The first release of the year in February contained all of the main changes from the summer (which is usually my most productive time).  In particular, this contained significant changes to the syntax of the language and a complete rework of the front-end to eliminate the niggling bugs I’d been having with it.  This was not fully completed until after a a few further minor releases and, overall, I’m very happy with the new syntax.

• Improvements to Verifier.  In July, v0.3.26 was released and with this came some major improvements to the verifier, and work on this continued through v0.3.27 and v0.3.28 in August.  Whilst this made a big difference to verification, I was also rather disappointed that I couldn’t get all cases I wanted to work.  In particular, there remain some problems related to quantifier instantiation which still need to be resolved (see #379).

• Simplifications to Language.  Towards the end of 2014, I began simplifying the language in various ways, in part to reduce the implementation burden.  Implicit coercions were dropped and cast expressions clarified in v0.3.30, and try/catch blocks were dropped in November (to be released).  This will continue in 2015 in an effort to make the language more concise and more manageable.

• Draft Language Specification. The first useful release of the language spec came came with the Feb release of Whiley.  Work on this continued throughout 2014, and a lot of the language is now covered (you can follow changes here).

A few other highlights from the year include the work of Matt Stevens getting Whiley code running on a QuadCopter, the work of Henry Wylde on integrating the Z3 Automated Theorem Prover, and that Whiley was used for teaching in the course SWEN224 @ VUW.  A lowlight of the year is probably the Eclipse plugin, which has been largely neglected.  The reason for this is that the Whiley Play web interface has proved a much more effective way to get people started with Whiley.

Overall, a productive year — but there is so much more to do!## Goals for 2015 The main goal for early 2015 is to make the next major release of Whiley (v0.4.0).  This has been a while coming, and I’ve held off for as long as possible whilst I try to stabilise the language and compiler.   I’m setting a provisional release date for v0.4.0 for the 1st February.  I want this to be an important milestone which locks down much of the language syntax, and delivers something genuinely useable.  Over the summer so far, I’ve made significant progress towards this and the next release (v0.3.32) will get us tantalisingly close.  In particular, the main things still to come for v0.4.0 are:

• Further Language Simplifications.  Continuing the work started at the end of 2014, there will be further language simplifications. For example, I want to remove string and char types and, instead, use lists of constrained ints to represent strings (see #432).  I’m also going to remove the protected modifier for now, as this is currently completely broken (#448).

• Updated syntax for methods and functions.  Thanks to Tim Jones, the syntax for methods and functions will change from e.g. function f(int x) => (int r) to use -> instead (as this is more consistent with other languages, like Haskell and Rust).

• Interpreter for WyIL bytecode.  Thanks to Sam Weng for contributing an interpreter for WyIL bytecode.  This will provide a reference implementation for the language, and help decouple the core compiler from the various backends and their implementation specific bugs, etc.

• Nested Bytecode Blocks.  Issue #190 was first opened in 2012, and is now finally being implemented! This will resolve a number of outstanding problems and bugs, and lead to simpler and more coherent mechanisms within the compiler.  It also opens up some interesting possibilities to help in generating source code from WyIL bytecodes (e.g. for use in a JavaScript backend, etc).  Finally, as part of this, I’ve also resolved the issue of storing bytecode annotations in binary WyIL files.

• Simplified Compiler Pipeline. As part of the process of simplifying the language itself, I have also been simplifying the compilation pipeline.  In particular, the BackPropagation phase has been eliminated (see #416).  Although this leaves more work for the backends, it simplifies the bytecode stored in WyIL files.  In addition, types will not be expanded in the front-end.  This will lead to better error messages, and allow me to eliminate a significant chunk of code from the front-end.  It will also mean that nominal information (i.e. names) are retained at the WyIL level, which is generally useful.

• Refactored Verification Condition Generator.  The verification condition generator has been significantly overhauled.  This was necessary in part to support nested bytecode blocks, however I’ve gone further in making its design more coherent.  This will allow more readable verification conditions to be generated, and also permit more reuse between verification conditions leading to better overall performance.

That covers most of the important things for v0.4.0.  Although many of them are “under-the-hood” improvements, overall they should yield a more reliable and complete implementation of Whiley.  Once v0.4.0 has been released, there are a number of additional things I’ll focus on in 2015, including:

• Improved Git Workflow.  In 2014, I started using a relatively simple Git workflow to help manage pull requests and releases, etc.  This boils down to a master branch holding the latest stable version, and the use of feature branches for managing new features.  In principle, I’ll also use a develop branch for staging new features and testing before final release.  This essentially works, but still causes problems with multiple developers.  In particular, one problem is that I often rewrite history on my feature branches because I develop across two different machines.  One approach to address this, for example, is to only develop on a personal Whiley fork before pushing to the master repository.  On my personal repository I can then rewrite history as necessary without risking others seeing the intermediate states.

• Continuous Integration.  Currently, testing is performed in a somewhat adhoc fashion.  Essentially, my current release procedure is: firstly, to make sure all tests are passing and, in some cases, mark those failing as @ignore;  secondly, to run ant dist to generate the distribution tarball; and, thirdly, to expand the tarball and run ant to check it builds from scratch.  Obviously, there are several manual steps here and I sometimes make a mistake and forget something.  To protected against this, we need to get a little more serious and starting using Continuous Integration (e.g. Travis CI).

• Split Compiler into Plugins.  One thing I worked on occasionally throughout 2014 is a plugin framework for the Whiley compiler.  I’m calling this the Whiley Compiler Collection and, instead of a single monolithic compiler, it will made up of a number plugins which together form the Whiley Compiler (and more).  The primary benefits of this is to provide a simple mechanism for others to develop and mantain their own plugins (e.g. for different backends, etc).  Currently, developing a backend essentially means merging it into the master compiler repository, which leads to a lot of code for me to maintain!

• Finalising Syntax.  There are still some important aspects of the syntax which remain to be finalised.  For example, there is currently no operator to check whether a map contains a given key or not.  Likewise, for loops do not support pattern matching properly (see #397), continue statements simply don’t work (see #327) and enumerations are broken (see #315)!

• Embedded Systems. Another focus for me in 2015 will be the use of Whiley for developing embedded systems.  This requires quite a bit of work.  For example, although a prototype C backend already exists for Whiley, this is of no use for compiling to embedded systems (i.e. because it makes extensive use of dynamic memory allocation).  Furthermore, the language itself does not lend itself naturally to embedded systems because of the limit support for memory management.  Currently, one can dynamically allocate memory via the new keyword, but this is no way to free such memory.  My plan is to support something similar to Rust’s object lifetimes (see #309).

Phew — I think that’ll do for now!!