Michelson has different type of annotations. I am curious about what is the main purpose of annotations and where should one use annotations vs where on shouldn't? Is there a michelson pattern where annotations are most useful? I do understand they serve purpose by adding more constraints to typechecking. Can someone provide a example where annotations are necessary?
Annotations are never necessary, they only add new type constraints.
Their purpose is twofold:
- documenting what corresponds to what in a Michelson smart contract (and I personally feel that this is really useful and should even be improved);
- adding constraints to ensure that these annotations are coherent with one another (it's also quite useful and these constraints enables some conservation of annotations when the stack evolves).