一句话：在 F* 证明助手中编码 WHILE 语言的操作、指称与公理语义，展示定理证明可辅助语义教学与研究。
程序语言语义是计算机科学的核心课题，但形式化程度极高，学生往往需要反复手写大量证明才能深入理解，过程繁琐且易出错。本文主张将现代定理证明器引入语义的教学与研究：作者在流行的 F* 证明助手中，对 WHILE 语言的操作语义、指称语义与公理语义三种风格分别进行编码，并在同一框架下机器化验证。案例表明，一旦程序及其语义被编码，现代证明助手只需极少人工干预即可证明若干有趣的程序语言性质。作者认为，以证明助手为工具教授程序语言语义，不仅能带来更具体的理解，也能培养未来研究者把定理证明器当作研究中的基础工具，而非事后补充。
The semantics of programming languages is one of the core topics in computer science. This topic is formalism-heavy and requires the student to attempt numerous proofs for a deep understanding. We argue that modern theorem provers are excellent aids to teaching and understanding programming language semantics. As pen-and-paper proofs get automated via the theorem prover, it allows an experiment-driven strategy at exploring this topic. This article provides an encoding of the semantics of the WHILE language in the most popular styles—operational, denotational, and axiomatic—within the F* proof assistant. We show that once the program and its semantics are encoded, modern proof assistants can prove exciting language features with minimal human assistance. We believe that teaching programming languages via proof assistants will not only provide a more concrete understanding of this topic but also prepare future programming language researchers to use theorem provers as fundamental tools in their research and not as an afterthought.