一句话：为 POSIX shell 定义可执行、机器化的小步操作语义 Smoosh，并通过测试验证其最符合 POSIX 标准。
POSIX shell 是管理系统的关键基础设施，功能强大但语义复杂微妙，长期缺乏精确形式化定义。本文为 POSIX shell 定义了机器化、可执行的小步操作语义 Smoosh，并实现对应解释器与符号步进器，以揭示其不直观行为。作者将 Smoosh 与 bash、dash、zsh、OSH、mksh、ksh93、yash 七种追求 POSIX 兼容的 shell 比较，使用 POSIX 测试套件、Modernish 测试套件与自建测试套件进行评估。结果显示 Smoosh 的语义最符合 POSIX 标准：Modernish 判定其 bug 最少（仅一个，来自 dash 解析器）且无怪癖。该工作为 POSIX shell 的形式研究、新 shell 与新工具开发提供基础。
The POSIX shell is a widely deployed, powerful tool for managing computer systems. The shell is the expert’s control panel, a necessary tool for configuring, compiling, installing, maintaining, and deploying systems. Even though it is powerful, critical infrastructure, the POSIX shell is maligned and misunderstood. Its power and its subtlety are a dangerous combination. We define a formal, mechanized, executable small-step semantics for the POSIX shell, which we call Smoosh. We compared Smoosh against seven other shells that aim for some measure of POSIX compliance (bash, dash, zsh, OSH, mksh, ksh93, and yash). Using three test suites—the POSIX test suite, the Modernish test suite and shell diagnostic, and a test suite of our own device—we found Smoosh’s semantics to be the most conformant to the POSIX standard. Modernish judges Smoosh to have the fewest bugs (just one, from using dash’s parser) and no quirks. To show that our semantics is useful beyond yielding a conformant, executable shell, we also implemented a symbolic stepper to illuminate the subtle behavior of the shell. Smoosh will serve as a foundation for formal study of the POSIX shell, supporting research on and development of new shells, new tooling for shells, and new shell designs.