Ergonomics of Spec Annotations

[mkovaxx]

The goal here is to discuss the ergonomics of spec annotations and document high-level decisions.

[mkovaxx]

Specs Are "Comment-Like"

Specs should behave like comments in the following sense. Removing all comments from a codebase never causes a compile error. The #[spec] annotations should behave the same way: if the code compiles with the specs, it should also compile with all specs removed.

Caveats

Removing some but not all specs may cause a compile error because of context-dependence. For example, a fn declaration in a trait may only have a spec if the trait itself has a spec annotation.

Comments have insert/remove symmetry: if the code compiles, inserting a comment cannot cause a compile error. The same does not hold for specs because of context-dependence. Each spec is validated (for syntax, name resolution, etc.), which means that inserting a spec can cause a compiler error.