The P4 programming language, a domain-specific language (DSL) for programming network devices, is at the core of the shift towards programmable networking. Nevertheless, the P4 language itself is inconsistently defined across four representations: the official specification document, implementations, tests, and formalizations.

Language mechanization frameworks can help resolve this inconsistency by defining a single specification model from which various representations can be derived. This has been exemplified by Sail for instruction set architectures (ISAs), ESMeta for ECMAScript, and Wasm-SpecTec for WebAssembly (Wasm). However, these successful efforts do not fit nicely into P4. At the heart of the problem is that P4 does not have an authoritative specification model specifying the complete and unambiguous language definition.

In this paper, we present P4-SpecTec, a language mechanization framework for P4. We propose a specification model based on \emph{algorithmic inference rule}, which is a restricted subset of inference rules that are executable. We mechanize the syntax and static semantics of P4 using algorithmic inference rules. This allows for the derivation of a type checker from the mechanized static semantics. We plan to mechanize the dynamic semantics of P4, and also support more P4-SpecTec backends, such as a parser, interpreter, and specification document. We envision adopting P4-SpecTec as the official P4 specification authoring framework, which would be the first effort towards adopting language mechanization into real-world programming languages without an authoritative specification model.