language-agnostic - 解决停机问题比人们想象的要容易吗？

Question

尽管一般情况是不可判定的，但许多人仍然解决了足以满足日常使用的问题。

在科恩关于计算机病毒的博士论文中，他展示了病毒扫描如何等同于停机问题，但我们有一个基于这一挑战的整个行业。

我也看过微软的终结者项目-http://research.microsoft.com/Terminator/

这让我要问——停机问题是否被高估了——我们是否需要担心一般情况？

随着时间的推移，类型会变得图灵完备——依赖类型看起来是一个很好的发展吗？

或者，换个角度看，我们会开始使用非图灵完备的语言来获得静态分析的好处吗？

Answer 1

Is solving the halting problem easier than people think?

我认为这和人们想象的一样困难。

Will types become turing complete over time?

My dear, they already are!

dependant types do seem like a good development?

非常如此。

我认为非图灵完整但可证明的语言可能会增长。很长一段时间以来，SQL 都属于这一类(不再是)，但这并没有真正削弱它的实用性。我想这样的系统肯定有一席之地。