Whiley is a hybrid object-oriented and functional programming language. Whiley employs extended static checking to eliminate errors at compile time, including divide-by-zero, array out-of-bounds and null dereference errors. Extended static checking is made possible through the use of an automated theorem prover. Whiley compiles to the Java Virtual Machine and is fully inter-operable with existing Java applications.
This video provides a general introduction to Whiley, including the syntax, some issues related to implementation and inter-operation with Java.
Video source and link to slides: http://whiley.org/2011/12/22/whiley-talk-wellington-ju/