为 Scade 6 编译器提供形式化认证工具的考虑 (2010)
在2010年左右(注1)，巴黎高师 Marc Pouzet 与 INRIA Nardelli 提出了一项长期项目的想法：为 Scade 6 编译器提供形式化认证工具(注3)。并欢迎对编程语言的设计与实现感兴趣、最好有函数式编程经验、Coq（注2）或Isabelle经验的学生参与进来。
注1: 2010年是一个估计的时间。在原始材料中列出的参考资料，最晚的一篇为2010发表，因此想法不早于2010年。另一方面，材料描述中提到 Scade 编译器是 Esterel Tech 的产品，而 Esterel Tech 于2012年被ANSYS收购，因此想法应早于2012年。综合前面描述的情况，该想法发生在2010-2012之间。巧合的是，清华L2C项目也是从2010年起启动。
注2：Coq 已改名为 Rocq. Rocq
注3：原材料可参考: Translation validation for synchronous data-flow equations in a Lustre compiler
这项想法源自于提出者对 Scade 编译器认证成本的观察。Marc 注意到，同步数据流语言 Scade 已经是安全关键领域软件的事实标准。Scade 编译器也遵循了如 DO-178C范式 Level A 标准的最高安全(safety)要求。这项认证过程对 Scade 取得商业成功有帮助，但也注意到，即使对 Scade 编译器进行少量修改，认证成本是主要成本。出于以上观察，想要探索一些方向对 Scade 编译器的形式化认证提供工具支持。更具体地，是要对 Scade 编译器内一些中间阶段设计翻译验证机制，即在编译期检查某个编译阶段的输入，与编译阶段后的输出的等价性。
作为入手的起点，目标是实现一个用于检查 Scade 编译器所执行的一些中间步骤之间的等价性的独立工具。Scade 编译器可以被视为对"时钟化的数据流方程(clocked data-flow equations)"(注4)的内部表示进行一系列源到源的转换，最终再转换为较为顺序命令式代码。设计的工具将直接作用于时钟化数据流的中间表示（IR）：
- 第一步将为时钟化方程定义一种范式、相关的变换函数。
- 接下来，将确定编译器需要提供哪些信息，才能使语义检查既易于实现和形式化。
- 可能需要依赖外部的 SMT 求解器，或在定理证明器中实现检查函数。
为了使项目更具可行性，将从一个简化的 Lustre 编译器入手，在初期仅考虑 Scade 6 的基本功能，而将更复杂的功能（如时钟演算、初始化分析、分层状态机等）留作后续扩展。
注4: 在一些翻译中，比如 L2C，对"equation"术语翻译为“等式”。但考虑到Scade面向的自动化控制算法建模中，术语"equation"在该领域指代“方程”；并且在ENS《同步反应式系统》(2024-2025)中，在介绍Lustre语言时，也提到其建立的方程组（equation set）不会无解，或有多个解，只有唯一解。因此，这里倾向于将“equation”以自动控制算法中的术语概念去理解，以"方程"描述。
在原材料中，也提到若干其他参考，比如LCTES 08[1]综述了 Scade 6 编译器的架构组成、各阶段机制、merge 与 reset 的关键作用、形式化描述的语义及形式化描述的转换函数等。也提到了语义分析中时钟演算机制[2]、初始化分析机制[3]等。以及层次化状态机的实现[4]。这些内容在ENS《同步反应式系统》(2024-2025)中也都有详细叙述。不过也需要注意到，前面的工作都是2010年前的状态，经过十多年的演化，Scade 6 编译器也有新变化[5]。由于不是本主题的相关内容，在这里不作展开。
[1]: Darek Biernacki, Jean-Louis Colaco, Gr´egoire Hamon, and Marc Pouzet. Clock-directed Modular Code Generation of Synchronous Data-flow Languages. In ACM International Conference
on Languages, Compilers, and Tools for Embedded Systems (LCTES), Tucson, Arizona, June 2008
[2]: Jean-Louis Cola¸co and Marc Pouzet. Clocks as First Class Abstract Types. In Third International Conference on Embedded Software (EMSOFT’03), Philadelphia, Pennsylvania, USA,
october 2003.
[3]: Jean-Louis Cola¸co and Marc Pouzet. Type-based Initialization Analysis of a Synchronous Data-flow Language. International Journal on Software Tools for Technology Transfer (STTT), 6(3):245–255, August 2004
[4]: Jean-Louis Cola¸co, Bruno Pagano, and Marc Pouzet. A Conservative Extension of Synchronous Data-flow with State Machines. In ACM International Conference on Embedded Software (EMSOFT’05), Jersey city, New Jersey, USA, September 2005.
[5]: Jean-Louis Colaco, Michael Mendler, Baptiste Pauget, and Marc Pouzet. A Constructive State-based Semantics and Interpreter for a Synchronous Data-flow Language with State machines. In International Conference on Embedded Software (EMSOFT), Hamburg, Germany, September 17-22 2023. ACM.