以最简单的程序为例，命题逻辑。至少有两种办法得到结果。一种是从公理出发，用逻辑规则推断。
另一种是真值表，0，1带入evaluate其结果。这个事实看上去简单。但是其严格证明，并不简单。
回到程序上来。显然，根据我们的日常经验，一个具有well defined的目的程序，（例如执行神经网络模型），往往可以有多种在语法范围内的no trivial的不同的实现。
现在的问题是，对于一个任务而言，在合乎语法这个范围内，不同的程序实现，这些实现之间，是否等价？
这条，我认为可以当作是程序语言的质量一个衡量指标。但是很遗憾，所有的程序语言，都不具备这种严格的等价性。
这个问题和数理逻辑的类型论，模型论，证明论都有关系。数理逻辑对逻辑系统有许多种衡量指标。
完备性，一致性，绝对一致性，等等一大堆。几十年后，距离实际应用越来越远。
任何一个程序语言，想要证明其类型安全什么的，在目前都是不切实际的目标。
对主流语言来说，要找个子集，并且证明这个子集的各种属性。那基本上就是5-7年一个phd的工作量。
可以认为这个问题，导致了c有很多undefined行为。类型不安全，往往会导致内存问题，以及各种内存security问题。cpp也是如此。
评论 (0)