In this blog series, we are presenting the five P4 projects accepted for this year’s Google Summer of Code (GSoC). The fourth one is Enhancing P4-SpecTec Usability: A Mechanized Specification for Nano-P4.
GSoC Project
Enhancing P4-SpecTec Usability: A Mechanized Specification for Nano-P4
P4-SpecTec provides mechanized formal semantics for the P4 language, but its adoption is currently limited by a lack of accessible learning resources. New users face a steep learning curve in understanding how to write, execute, and utilize mechanized specifications in practice. This project proposes to improve the usability of P4-SpecTec by developing a tutorial-style documentation centered around nano-P4, a minimal subset of the language.
The tutorial will guide users through writing mechanized specifications, executing them, and generating specification documents, providing a hands-on introduction to the framework. The technical scope includes constructing a complete nano-P4 specification within P4-SpecTec, designing detailed examples, and demonstrating workflows for specification execution and document generation. The end result will be a practical and reproducible learning resource for onboarding new users.
Project Mentor: Jaehyun Lee
Contributor: Haechan Kwon
Haechan is an undergraduate student at KAIST School of Computing. His interests are in programming languages and bridging the gap between practice and theory.
