主要观点：

• 编程时面临的挑战之一是确定程序运行时的行为，程序员通常通过运行程序并修改来解决。
• 语言实现者面临更具挑战性的问题，即如何确定语言实现的正确性，通常有隐含的正确性标准和语言描述可作比较。
• 多数语言规范是部分正式的，像 Standard ML 这样有正式规范的语言很少，大多数工业语言规范是非正式的。
• 对于独立或业余语言开发者，即使是非正式规范也难维护，而缺乏规范会导致边缘情况的正确性问题。
• 在 Futhark 中，因编译器优化导致很多边缘情况处理方式不统一，需要明确语义。
• Futhark 采用完全不同的评估语义实现即解释器作为语言的参考实现，解释器慢但适合调试和小输入测试，编译器和解释器行为不一致时可修改，编译器在某些情况下可与解释器不同。
• 缺乏正式规范时，通过产生两个实现可确保语义是有意的而非偶然的，Futhark 的解释器和编译器共享前端。

关键信息：

• 编程中程序运行行为确定及解决方法。
• 语言实现者确定语言正确性的方式。
• 不同语言规范的形式及特点。
• Futhark 中编译器和解释器的情况及作用。

重要细节：

• 多数工业语言规范多为非正式，如 C 等。
• Haskell 虽为学术宠儿但也无正式规范，部分子部分有单独规范。
• Futhark 早期边缘情况处理方式及优化与语义的关系。
• 解释器编写风格直接，代码丑但体现语义。
• 编译器和解释器行为不一致时的修改原则及特殊情况。