lol
Exploratory programming is fine, but I don't need to explore anymore what a theorem is :-)
> "Arc will not allow anything that limits what the user can do"
Obviously this is not true, as Arc limits me such that I cannot create a safe theorem type. What this means is that I cannot let the user directly interact with Arc when building an interactive theorem prover; I have to wrap some kind of protective layer around it, which would probably hinder lots of the exploring!
