While it might seem like there were already plenty of languages riding atop the JVM, ranging from JRuby to Scala, Groovy to Kotlin, the developers of the open source Whiley language believe they still have something new to offer by tackling the verifying compiler challenge.
A verifying compiler uses mathematical and logical reasoning to check program correctness. "The question I'm trying to answer is whether or not it's possible to build a verifying compiler that could genuinely be used in practice," said main developer David Pearce, a senior lecturer in computer science at the University of Wellington, in New Zealand. "That means it's got to generate reasonably efficient code, it's got to have all the bells and whistles we expect from a modern language, and the compile-time verification has got to work well enough that it adds value and doesn't get in the way."
Whiley uses extended static-checking to eliminate errors at compile time, and like Scala, it leverages both object-oriented and functional programming. Pearce sees it as best suited for apps where safety and security are critical. "For example, the infamous Heartbleed bug contained a buffer overrun, which is exactly the kind of thing that Whiley checks for," he said.