Doesn't scheme have a set macro? I think for purity you'd have to go to something used for proofs that doesn't actually interact with the world.