Will that theorem prover be usable someday so I would be able to implement my version of Singularity in Nemerle? I would call it DOS = Dependable OS... :)