Clean Language
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.