不能判定就超时让程序员掐掉呗, 理论上任何人编程序的时候都没法判定他编的程序能不能用啊 //@tertio: 回复@slit-eyed: 定义一个类型T1为可停机的程序，那么T1无法判定；定义类型T2为X命题是否成立，那么T2的判定也许就成了强AI。类型系统过强就会如上，如果不强，就是现在这种半残废的样子。
