Whiley

Whiley is a programming language created in 2009 by David J. Pearce.

Source code:

git clone https://github.com/Whiley/WhileyCompiler

#731on PLDB

15Years Old

2Repos

Try now: Web

Whiley is an experimental programming language that combines features from the functional and imperative paradigms, and supports formal specification through function preconditions, postconditions and loop invariants. The language uses flow-sensitive typing also known as "flow typing." The Whiley project began in 2009 in response to the "Verifying Compiler Grand Challenge" put forward by Tony Hoare in 2003. The first public release of Whiley was in June, 2010.Primarily developed by David Pearce, Whiley is an open source project with contributions from a small community. Read more on Wikipedia...

Whiley website
Whiley Wikipedia page
Whiley is developed on GitHub and has 199 stars
There are at least 2 Whiley repos on GitHub
file extensions for Whiley include whiley
Whiley on Twitter
The Google BigQuery Public Dataset GitHub snapshot shows 1 users using Whiley in 1 repos on GitHub
Pygments supports syntax highlighting for Whiley
whiley.org was registered in 2009

Example from the web:

// Define the type of natural numbers
type nat is (int x) where x >= 0
public function indexOf(int[] items, int item) -> (int|null index)
// If int returned, element at this position matches item
ensures index is int ==> items[index] == item
// If int returned, element at this position is first match
ensures index is int ==> no { i in 0 .. index | items[i] == item }
// If null returned, no element in items matches item
ensures index is null ==> no { i in 0 .. |items| | items[i] == item }:
    //
    nat i = 0
    //
    while i < |items|
    // No element seen so far matches item
    where no { j in 0 .. i | items[j] == item }:
        //
        if items[i] == item:
            return i
        i = i + 1
    //
    return null

Example from hello-world:

import std::ascii
import std::io

method main(ascii::string[] args):
    io::println("Hello World")

Feature	Supported	Token	Example
MultiLine Comments	✓
Binary Literals	✓		// [01]+b
Integers	✓		// [0-9]+
Floats	✓		// [0-9]+\.[0-9]+
Hexadecimals	✓		// 0x[0-9a-fA-F]+
Strings	✓	"	"Hello world"
Print() Debugging	✓	io::println
Comments	✓		// A comment
Line Comments	✓	//	// A comment
Semantic Indentation	X

Whiley - Programming language

Language features