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
Currently a research engineer at ConsenSys, Dr. David J. Pearce's research interests are in programming languages, compilers, static analysis tools, and formal verification. He is the creator of the Whiley programming language, which provides support for providing functional specifications in the form of preconditions and postconditions, and is designed to simplify verifying software. His site includes a page on Whiley, which includes videos of related talks.
https://whileydave.com/
GitHub: The Whiley Programming Language
Devoted to the development of Whiley, an open-source programming language developed by Dr. David J. Pearce, this is the official GitHub repository for Whiley. Included are the source code, compiler, a compiler backend, and other tools available under the Apache 2.0 license, along with WhileyWeb, a simple web IDE for running Whiley programs on the computer using a web browser, available under the BSD 3-Clause license, and documentation for the Whiley programming language.
https://github.com/Whiley/
This is a fork from the programming language by the same name, created by Dr. David J. Pearce, relicensed to use a BSD license, the GitHub repository was created by Edmund Horner. Whiley is a programming language particularly suited to safety-critical systems. It is a hybrid object-oriented and functional programming language that employs extended static checking to eliminate errors at compile time, including divide-by-zero, array out-of-bounds, and null dereference errors.
https://github.com/ejrh/Whiley
SlideServe: The Whiley Programming Language
SlideServe is a free online platform that allows users to upload, share, and discover professional digital content such as presentations and documents. Typically, experts create and share their presentations and documents on topics they wish to speak about. This is a presentation about the Whiley programming language created by Donovan Rice. Whiley is a statically typed language designed to allow programmers to write reliable and safe code. The presentation may be viewed or downloaded.
https://www.slideserve.com/donovan-rice/the-whiley-programming-language
Designed by David J. Pearce in 2010, Whiley is a programming language with extended static checking. Influenced by C, Java, Python, and Rust, the language supports formal specification through function preconditions, postconditions, and look invariants, and is available as open-source software through the Berkely Software Distribution (BSD) License. Development notes and announcement, beginning in June 2010, are published to the site, and a download link is provided.
https://whiley.org/
