Whiley

Whiley is a hybrid object-oriented and functional programming language which compiles to the JVM. Whiley employs extended static checking to eliminate errors at compile time, including divide-by-zero, array out-of-bounds and null dereference. Whiley's Extended static checking is made possible through the use of an automated theorem prover.