Uninterpreted function signature

[utaal]

At the moment, we allow uninterpreted functions to be written as:

• open spec fn name(a: int) -> (b: int)
• closed spec fn name(a: int) -> (b: int)
• spec fn name(a: int) -> (b: int)

The first doesn't really make sense (the function does not have a body). The last two could be considered equivalent. Relatedly, we plan to disallow the open/closed modifier on trait function declarations, but these will "get a body" given by the trait implementation, while free or associated (i.e. in an impl) uninterpreted functions never have a body.

We are currently considering two options:

• only allowing spec fn name(a: int) -> (b: int);
• only allowing uninterpreted spec fn name(a: int) -> (b: int); or some other similar marker, to highlight that the function is, in fact, uninterpreted.

The former is shorter (and is currently valid) but might be considered to be confusing because a similar declaration in a trait has a different meaning, the latter requires more typing, and would require a deprecation cycle.

I recommend we stick to either of these two options, so we can resolve this quickly. You're welcome to suggest alternatives, but they need to be well-motivated. Additionally, if you prefer the second option (adding a marker), we are looking for suggestions on what the marker should be.

[utaal]

How about def spec fn name(a: int) -> (b: int);?

[tjhance]

Though this use-case is somewhat niche, the current situation means it is not possible to declare a trait function with a 'default body' that is uninterpreted.

[jaybosamiya-ms]

My vote is to require a specific keyword (i.e., the uninterpreted spec fn ... version).

My two main concerns are:

1. Discoverability in the documentation. Searching for a keyword uninterpreted in the docs is easier than "function without a body but only a semicolon".
2. (Minor) Making the uninterpreted functions obviously stand out. I have been bitten in the past by missing a semicolon visually. By having a specific keyword needed, we make it incredibly obvious that this is special.

I am not particularly about the extra typing necessary (at least imho, uninterpreted functions are not the "common case" for most verified code, thus we don't need to make it be the absolute minimum length needed and can actually afford to keep it longer, to obtain the above benefits).

No strong opinions on the specific keyword used (imho, uninterpreted is fine even if on the long side; uninterp may be a bit less wordy, untrp is probably un-understandably short).

Tangent (click to open)

I experimented with ChatGPT for an alternative keyword, and it suggested "mysterious" 😆 Prompting it further gave "vague" and "incomprehensible" 🤣

[utaal]

Would everyone be onboard with uninterp spec fn name(a: int) -> (b: int);?

cc @Chris-Hawblitzel @tjhance @jaybosamiya-ms @jonhnet @jaylorch ? React 👍 for yes, and 👎 for no: if you vote no, please provide an argument.

[jaylorch]

"Uninterpreted" is the word Z3 uses for it, but I'm not sure that adjective is sufficiently evocative to be understandable to a lay user. I'm not sure what would work, better, though; perhaps "unspecified" or "undefined"?