Abstract:Synchronous data-flow languages, such as Lustre, have been widely used in safety-critical industrial areas, such as airplanes, high-speed railways, and nuclear power plants. The safety of development tools themselves for these types of applications is highly required. In better solving the "miscompilation" problem, very successful progress has been made recently to implement the construction and verification of a conventional imperative language compiler, such as the CompCert C compiler, by using reliable-by-construction proof assistants. L2C is a trustworthy compiler developed based on such an approach, with an extended Lustre language as its source, and Clight, a C subset used in ComperCert, as its target. L2C is an industry-level synchronous data-flow language compiler developed by using the same technique. The paper focuses on the key translations of L2C and the main issues and experience in its design and implementation.