Proving case statements

One important but silly obstacle in applying theorem-proving formal methods to program analysis is simply the User Interface. How should a user express properties about a program that he or she wishes to prove true? How should the user give hints to the theorem prover to guide it along if it gets stuck? One idea for Haskell, albeit possibly a low-hanging fruit, involves data constructor alternatives for case statements. The compiler can already detect when a series of case alternatives does not cover all possible cases. We go the next logical step and try to prove that those omitted branches are actually not reached. Sometimes, the theorem prover might be able to prove that a certain branch X is unreachable if some other branch Y in a different case statement (perhaps in the calling function) is also unreachable. The user can help the theorem prover along by annotating that branch Y with the error function which tells the theorem prover to add that assumption. If that assumption is violated at run time, the error function will be called.