工业界可信的都不是编译型的，都是解释型的，例如波音和空客航空器使用软件系统。




【 在 annals 的大作中提到: 】
: 我最近也在看这个,工业界的应用主要是写出可信的无bug的程序,数学家的话用来确保一些很复杂的证明是可信的没有gap,现有比较有名的例子是四色定理和奇阶定理(odd order theorem)
:
--
FROM 111.18.168.*