Toward a More Carefully Specified Metanotation

POPL is known for, among other things, papers that present formal descriptions and rigorous analyses of programming languages. But an important language has been neglected: the \emph{metanotation} of inference rules and BNF that has been used in over 40\% of all POPL papers to describe all the other programming languages. This metanotation is not completely described in any one place; rather, it is a folk language that has grown over the years, as paper after paper tries out variations and extensions. We believe that it is high time that the tools of the POPL trade be applied to the tools themselves. Examination of many POPL papers suggests that as the metanotation has grown, it has diversified to the point that problems are surfacing: different notations are in use for the same operation (substitution); the same notation is in use for different operations; and in some cases, notations for repetition are ambiguous, or require the reader to apply knowledge of semantics to interpret the syntax. All three problems present substantial potential for confusion. No individual paper is at fault; rather, this is the natural result of language growth in a community, producing incompatible dialects. We back these claims by presenting statistics from a survey of all past POPL papers, 1973--2016, and examples drawn from those papers. We propose a set of design principles for metanotation, and then propose a specific version of the metanotation that can be always interpreted in a purely formal, syntactic manner and yet is reasonably compatible with past use. Our goal is to lay a foundation for complete formalization and mechanization of the metanotation.