Skip to content

The Whiley Programming Language: Design & Implementation

Photo of
Hosted By
Andrew H.


June's MelbJVM features an international speaker from New Zealand, David Pearce, presenting on his programming language Whiley which runs on the JVM. It's statically typed but is influenced heavily by low noise dynamic languages like Python, as well as the use of type constraints as a first class citizen to enforce compile type checking on things you wouldn't normally expect to be checked until runtime.


Whiley is a new programming language being developed at Victoria University of Wellington, New Zealand (see ( Whiley is designed specifically to simplify program verification. This goal has constrained the language in many ways, some of which will be expected whilst others are less apparent. The language includes first-class pre- and post-conditions, and the aim is to automatically check them at compile time. Such constraints must be pure and may range over first-class data-types (sets, lists, etc) with value semantics, and also functions that are explicitly declared pure. To simplify verification, arithmetic operates over unbounded integers and rationals. For flexibility, a flow-sensitive type system with structural subtyping is employed.

Despite being a primarily functional language, Whiley retains a distinctly imperative syntax with the look and feel of a dynamic language (i.e. Python). Whiley currently compiles to the JVM and is fully inter-operable with Java. Many challenges exist in compiling Whiley programs to the JVM for efficient execution. Furthermore, other compilation targets (e.g. JavaScript) are planned for the future. In this talk, I will introduce and demonstrate Whiley, as well as discuss some of the main challenges involved.


David graduated from Imperial College London in 2005, and took up a lecturer position at Victoria University of Wellington, NZ. David's thesis was on efficient algorithms for pointer analysis of C, and his techniques have since been incorporated into GCC. His interests are in programming languages, compilers and static analysis. Since 2009, he has been developing the Whiley Programming Language ( ( which is designed specifically to simplify program verification. David has previously interned at Bell Labs, New Jersey, where he worked on compilers for FPGAs; and also at IBM Hursely, UK, where he worked with the AspectJ development team on profiling systems.

Info on getting there:

Peoplebank offices are on the south-west corner of Flinders Lane and Queen St. Doors lock at 6pm but someone from Peoplebank will be downstairs to let people in. If when you get there, no one is present, call 0432603743 and we'll send someone down. We also will be having a raffle, so when you get to Level 13, there will be someone to greet you, get a nametag, and also put you in the raffle draw. For those driving in, there is $10 flat rate after hours parking on Market St, between flinders lane and flinders st.

Level 13, 31 Queen St · Melbourne