Whiley

Creating high integrity software at scale.

function max(int x, int y) -> (int r)
// Ensure return not smaller than parameters
ensures (r >= x) && (r >= y)
// Ensure a parameter returned
ensures (r == x) || (r == y): 
   if x >= y:
      return x
   else:
      return y

Reliability

Whiley employs state-of-the-art techniques for ensuring your software is correct. You can specify functions using preconditions and postconditions, and then statically verify( your implementation meets its specification.

Open Source

Whiley is an independently developed open source project and is free to use. Join our community on our Discord channel, follow us on Twitter and contribute to the code on GitHub.

Flexibility

Whiley supports functional and imperative programming without being opinionated. Whiley can be used to develop web applications, smart contracts, embedded systems and more.

Features

Specification. Unlike most other programming languages, Whiley provides first-class support for specifying functions using preconditions and postconditions.
Static Typing. Whiley is a statically typed programming language which employs type inference and flow typing for ease of use.
Static Verification. Whiley supports static verification technology to give sophisticated support for finding software errors.
Automated Testing. Whiley supports automated testing (in the style of QuickCheck) to quickly check for errors and other problems.
Package Management. Whiley has a small but growing selection of packages developed in the community. The Whiley build tool allows you to easily manage your dependencies and distribute libraries.