Aviva Directory » Computers & Internet » Programming » Whiley

Designed by David J. Pearce, the Whiley programming language is an open-source project with contributions from a small developer community.

Whiley is an experimental programming language that began as a response to the "Verifying Compiler Grand Challenge" put forward by Tony Hoare in 2003. The project began in 2009, the first release was in 2010, and the first stable release was in 2022. Influenced by C, Java, Python, and Rust, Whiley is licensed under a BSD license.

The Whiley system has been used for student research projects and in teaching undergraduate courses. The Whiley compiler generates code for the Java virtual machine and can interoperate with Java and other JVM-based languages.

The goal of the Whiley project was to produce a realistic programming language in which verification is used routinely and without thought, an ideal that was promoted in the early 2000s by Tony Hoare, who described his Grand Challenge as "a verifying compiler uses mathematical and logical reasoning to check the correctness of the programs that it compiles."

Other attempts to develop such a tool produced SPARK/Ada, ESC/Java, Spec$, Dafny, Why3, and Frama-C. Most of these focused on extending existing programming languages with constructs for writing specifications. In contrast, Whiley was designed from scratch in an effort to avoid common pitfalls and to make verification more tractable.

Whiley's syntax is similar to imperative or object-oriented programming languages. In Whiley, indentation syntax is chosen over the use of braces to delineate statement blocks, which gives it a strong resemblance to Python, but the imperative appearance of Whiley is deceptive since its language core is functional and pure.

In Whiley, a function, which is pure, is distinguished from a method, which may have side-effects. This is necessary in order to allow functions to be used in specifications. A familiar set of primitive data types is available in Whiley, including bool, int, arrays such as int [], and records like {int x, int y}, but, unlike most programming languages, the integer data type, int, is unbounded and does not correspond to a fixed-width representation. For this reason, an unconstrained integer can take on any possible integer value, subject to the memory constraints of the host environment. This simplifies verification, given that reasoning about modulo arithmetic is a known and hard problem. In Whiley, compound objects, such as arrays or records, are not references to values on the heap, as they would be in C# or Java, but are immutable values.

This portion of our web guide focuses on the experimental programming language known as Whiley. Online resources focusing on the Whiley programming language are appropriate for this category, along with any tools or editors intended to facilitate Whiley programming, as well as tutorials, user groups, the Whiley developer community, reviews, or other websites, or sub-sections of websites, whose focus is on Whiley.



Recommended Resources

Search for Whiley on Google or Bing