ocaml-gospel / gospel

A tool-agnostic formal specification language for OCaml.
https://ocaml-gospel.github.io/gospel
MIT License
123 stars 16 forks source link

Too much ghost keywords? #395

Open n-osborne opened 4 months ago

n-osborne commented 4 months ago

Duplicated from discussion on #393:

I've spotted that there is the val keyword for introducing ghost declaration. I believe this is a relic of a previous version of the language as it is used in the vocal tests and in just one example from the walkthroughs/union-find.md documentation file but not really documented as a keyword introducing a ghost value.

I'm not sure we want to keep it, as there is no appearent distinction with function and we're already wondering whether to keep predicate in #391.

I believe we can move forward with removing the val keyword. (Or we can go the other way around and remove the function keyword).

Offline discussion didn't reach a strong agreement (nor a strong disagreement) on the predicate one.

predicate can indeed been seen as a nice, though not necessary, syntactic sugar for functions returning a bool (once #391 has been merged). The cost of maintaining it doesn't seem to be too hight neither. The decision may be reduced to the question whether we want to simlpify the existing syntax. This may not be a bad idea as there are some new syntax that are worked on that are really related to conceptual subtleties (e.g. ownership).