我认为，现在是编程语言和形式方法非常有趣的时刻，因为大型语言模型（LLMs）完全改变了软件的约束环境。这一点已经可以看到一些迹象，例如，将C语言移植到Rust的势头上升，或者对升级COBOL等遗留代码库的兴趣日益增长。特别是，LLMs在翻译方面*特别*擅长，相较于从头生成，因为1）原始代码库充当了一种高度详细的提示，2）作为编写具体测试的参考。也就是说，即使是Rust作为目标语言，对于LLMs来说也远未达到最佳。那么，什么样的语言是最优的？对于人类来说，仍然有哪些让步（如果有的话）？这是令人难以置信的新问题和机会。我们很可能会多次重写所有曾经编写的软件的大部分。