That's a truly amazing effort to take on the OS problem from a theorem-proving standpoint. I of course would try to attack the same problem on a theory-indiffe

That's a truly amazing effort to take on the OS problem from a theorem-proving standpoint. I of course would try to attack the same problem on a theory-indifferent substrate. But... +1 for an exciting vision of math uber alles.