On 6/17/2011 4:27 AM, Don wrote: > That'd probably work if the compiler already had a theorem prover -- but it > doesn't. I've tried out the theorem prover in Spec#. It only works in trivial cases.