Naming of function modes and variable modes

[tjhance]

It's pretty important we get the names of the modes right, since new users will need to come to terms with them quickly. I think the names we have don't necessarily convey the right intuitions up front.

I'll post a specific proposal in a comment.

[tjhance]

I think we should consider that the mode names for variables don't necessarily need to be the same as the mode names for functions.

Specifically, I think #[proof] variables and #[proof] types might be confusing to new users. Proof variables are kind of an advanced feature, and we don't want new users to reach for them just because they're "doing proofs". Furthermore, they might be confused by the fact that the default variable mode for a #[proof] function is #[spec] rather than #[proof].

Proposal. Rename #[proof] variables to #[ghost] (while #[proof] functions remain as they are).

Rationale:

• ghost is a more familiar term-of-art for people in the verification space
• Less confusion to new users (see above)
• #[proof] is a great name for lemma functions, so of course that should remain as it is

In such a proposal, it might make sense to rename #[spec] variables as well, but I don't have a good suggestion here. I just think it's a little weird that we use "spec" variables when writing proofs.

[tjhance]

con: the current scheme (of having the names be the same) has the nice property that a function of mode M can support variables of any mode M' >= M

[parno]

FWIW, Dafny is contemplating some changes in their naming too: dafny-lang/dafny#1564

[utaal]

We have chosen ghost and tracked for variables.