Remove FStar.Ghost.Pull #3636
Remove FStar.Ghost.Pull #3636
Conversation
|
I am curious why this axiom is removed? Is it because it introduces an unsoundness? |
|
Hi Theophile. There are no concrete plans to pull pull. That's why this PR is marked as draft. However, pull is one of the few axioms that we include in F* and I have been trying to figure out how much code relies on it. So far I couldn't find anything that makes essential use of pull (see also FStarLang/pulse#291 and project-everest/everparse#160). If you use pull, I'd be curious to learn more.
I believe that pull is sound. But the negation of pull piqued my interest. |
No, I am not using the I see, if I understand correctly this axiom is convenient, but in practice it can be replaced by something else, so this PR asks the question why we should keep it? |
Apparently, my comment was too opaque then. 😄 I want to add a parametricity axiom to F* that conflicts with pull. If pull was actually used, then that would be a big price to pay. But as this PR shows, we can easily remove pull and make room for this other axiom. |
|
Ah ok, thanks for the explanations! |
gebner
force-pushed
the
gebner_rm_ghost_pull
branch
from
f738d5c to
77f5528
Compare
|
We discussed this the other day and decided that if we can rework proofs without relying on the Pull axiom, then let's remove the axiom altogether. One todo: The PoP in F* book mentions pull here, and this should be revised |
This PR removes the pull axiom. The pull axiom is incompatible with other axioms that we might consider adding in the future. Removing it now leaves the door open for these future changes.
Without pull, the total and ghost function spaces no longer coincide. One way to think of this is as follows:
a -> Tot bis the space of the computable functionsa -> GTot bis the space of all (mathematical) functions