Whiley is a programming language being developed at Victoria University of Wellington, New Zealand (see whiley.org). Whiley currently compiles to the JVM and is fully inter-operable with Java. Whiley is being designed to help eliminate software errors. Whiley programs can be "verified" at compile time, and doing this prevents a range of common errors impossible (e.g. divide-by-zero, array out-of-bounds, etc). Unfortunately, the act of verifying a program presents its own challenges.
The Whiley project has been running since 2009 and, more recently, has been undergoing a number of changes to its syntax. In this talk, I will look at what verification means in Whiley using a series of interesting examples. I will also look at how the language is evolving and what is influencing this (e.g. embedded systems, Rust, etc).