Clean

The Clean Game Library is a complete development system for 2D games (arcade, side scrollers, platform games), using the functional language Clean. Allthough Clean is not easy to learn (it's very different from imperative languages, such as Pascal and C), once you have mastered programming in Clean, you can easily create games with the Clean Game Library.

More info 

Sparkle is a theorem prover for the functional programming language Clean (version 2.0). It can be used to prove the partial correctness of Clean applications. On a smaller scale, it can also be used to prove useful properties of smaller parts of programs. Sparkle has a sophisticated windows-oriented user-interface (meaning that all content is graphically displayed in windows that can be resized, moved and closed at will). The proving process is supported by a hint mechanism, which acts as a proof wizard and suggests proving actions to the user.

More info