I would rather have a formal spec as the definitive one. Deriving a formal spec from a readable one seems to hit ambiguous cases all the time. Just look at publ

I would rather have a formal spec as the definitive one. Deriving a formal spec from a readable one seems to hit ambiguous cases all the time. Just look at publications that do that for C or Java. With a formal spec you could also derive an implementation automatically which is a great useable reference. Look up the K framework for one possibility.