这个是 @裴喜龙 老师给的系统正确性论述。

系统正确性的三个层次：程序正确性、逻辑计算正确性、模型正确性。
程序正确性，是程序正常工作，无异常退出。
逻辑计算正确性，是程序与设计的一致性，如果出现不一致，则是出错。
模型正确性，是设计与需求层面的事，对客观事务的理解出错了，

程序正确性由测试解决，是代码上的事，是程序实现技术上的事，是运行时、操作系统的事。
在cdl语言级支持Frama-C，是解决“逻辑计算正确性”，用于验证程序逻辑与设计的一致性的。

++++

第一个程序正确性，如果确定定义为『程序正常工作，无异常退出。』个人理解，这个只要语言的类型系统sound就够了，这个应该就是safe的定义。最早这样表述的应该是Robin Milner，在他的ML语言的工作中。

第二个逻辑计算正确性，是程序与设计的一致性；这个用我熟悉的表达方式，似乎是应该表达为『程序满足Specification的要求』；specification和implementation在字面上容易理解，但specification可能很难定义，或者很难证明，或者这个证明不一定在语言层面完成。

因为大家在说系统而不仅仅是语言或者语言的runtime，系统首先就成为程序的依赖性，系统可能资源枯竭，starving，各个层面上的，内存不足，CPU跑满，io调度排队，包括文件系统和网络。另一方面，在实际的绝大多数系统应用中，非功能需求很少在早期出现在specification里，比如最多使用多少内存，或者能抗住多少请求，那请求和请求还不一样，能抗住多少什么样的请求；如果软件在专门做一层，存储，或者负载均衡，专业做这个领域的人员也许还能提出这种spec，并且知道测试和提升的办法。但大多数混在业务软件里的，压跟没有这类定义，都是遇到性能不行了才想这是怎么回事，怎么标定，怎么测试，怎么优化，或者怎么牺牲（例如保证有限可用性）。

一个应用软件的完备的spec，对于实际工程的资源投入而言，在大多数情况下就接近与无穷大。这是个工程现实，也很大意义上肯定了测试驱动而不是验证（Verification）驱动，因为测试驱动很灵活，就是哪里塌了哪里测，有的放矢。

很难证明的情况很多，证明一个算法不死锁活锁就干翻绝大多数程序员了；而且这些证明通常不在语言层面完成，可能要使用Process Calcluli，或者类似SPIN，TLA+这样先construct一个小模型，证明之后再Code Gen框架代码，再填充细节。

而且一些直觉上很简单的东西，比如『请你证明一下你的程序不会使用超过450MB内存』，Java程序员只会低声回答你给我滚。这虽然是个玩笑，但是也说明更多层的抽象会让verification也更困难，包括前面说的操作系统抽象也有同样的问题。

这些还都和实时性无关。绝大多数语言都未提供对实时性的定义。

这段在说我理解的『程序满足spec』，测试是不完备的，但是有技巧和经验的自动化测试在行业里工作的不错；只有很特殊的软件需要verification，无论是证明器的，还是模型检查的。证明器的，大名鼎鼎的作品就是seL4。还有Xavier Leroy领衔的CompCert，验证过的C语言编译器。

seL4是一个明星项目。站在工程的角度看用verification的巨大优势，不仅仅在于『绝对』正确上，也在于它可以用一条证明，替代天文数字的测例。不过后者其实很难说proof-based verification做到了，因为seL4的proof script的代码量也是seL4的源码量的几十倍，这个倍率，用test suite也可以做到相当好的质量了，而且写test suite容易招聘得多。

CompCert至今闭源。实际上国内学术界如果有人出头做一个copycat是有价值的，因为在很多领域真的需要编译器绝对正确，而编译的代码效率不够高可以用更高主频的处理器解决。但这也是一个艰苦的工作，工作量不小。也意味着类似的工作，很难在商业公司完成。

而且不要忘了这两个项目有个很好的特点是spec够小。高度抽象的软件都有一个特点就是小接口，但是deep，内部逻辑复杂。但小接口，或者小spec集合，才能给verification提供可能性。

如果是个GUI程序，CSS特效加持着各种动画飞来飞去，这怎么验证？我听说过有国外大媒体公司像素级验证web开发结果的（对照photoshop稿），但这么变态的要求也还不是全部，也只能挑典型分辨率，目标配置，还有动画呢？验证帧率吗？要是动画是交互的，要开发一个机器人去对打和录屏吗？

不多举例子了，观点已经很清楚了，我们都同意implementation should meet specification，但很多的时候不是practical的，spec不完备甚至无法完备；就算能完备成本上也没有必要。可以理解为verified software在今天看仍然不是普适的，只适用于有抽象稳定接口的系统软件，而且规模不大。你看数据库这么广泛使用的工业软件，都没有一个流行数据库证明过了。

++++

在软件工程意义上Design和Specification是两回事，但是工程实践上，其实Spec一样就应该意味着交付品一样，理想情况下可以drop-in replacement。

实际的外包软件之所以做到Design层面，不只是甲方不信任乙方的Design，Design是可行性验证的必要一环，没有Design，软件如何满足Specification，不是一眼可见的，而且还有可维护性，可扩展性等多种工程要求，所以实际软件都会有architecture，component/module，测试也是bottom-up，从单元到集成到系统，但这个也是完全工程导向的，单元可以verification，几个单元组起来满足更大的组件，那还得继续证明，不是不正自明的，因为涉及到通讯证明应该也会更麻烦。

有趣的一点是这个软件组件的drop-in replacement，在不大的尺度上，有形式化的定义，bi-similarity/bi-simulation，Miler在pi-calculus里给出了这个定义，基于Labelled Transition System。而且在过去十年，在计算机语言的类型理论研究中，session type是一个较新的方向，session type可以描述通讯的contract，而且强制通讯一方的实现满足这个contract，通过type checking。这是非常有意思的，而且很可能在工程上有高价值。虽然restful这种无态设计很流行，但应该说无态设计是简化的设计，bullet-proof，但性能是有牺牲的，有很多问题有态设计的效率高的多，比如大数据集同步。

而说到类型系统是一个很长的故事，我也在坑赤瘪肚的学习。这个部分入门有困难，因为逻辑的发展分岔了，有经典逻辑和直觉逻辑（甚至minimal logic，证明论教材里阐述的比较好）；而逻辑学家们致力于发展类型系统的目的在非常大的意义上是为了在定理证明器里表达数学（而不是程序）；de Brujin的Automath，Constable的NuPRL，Coquand的Coq，都是里程碑，也一路发展了类型论。计算机语言里的类型系统可以不从这些抽象的地方开始学，因为程序员也能用这门语言，但背后的符号逻辑是一样的，写这个语言的编译器，type checker的人肯定要懂类型论。

但尽管已经硕果累累和群星闪耀，类型能表达的内容，或者说表达力，仍然里程序员们希望能做到的对程序的约束，还差好远。同时毕竟这是语法方法，注定了和语义无关，而所有和语义有关的限制，generally的证明不了，rice定理，让人非常沮丧。

在正经计算机语言理论的书里，没有把语言还分为spec和implementation两个层面的提法，code is code；但是象rust那样双向链表都写不出来的语言，仅仅是type系统是过于strong了？我们直觉上都知道只要双向链表的插入删除操作能够原子化，这是不但合法而且高度有用的数据结构，难到我们就不能允许它有那么一个瞬间短暂的break rules？换句话说，我们把break rule的瞬间考虑在spec之外，比如，如果有个处理器就带有原子化的指令完成双向链表操作（bi-directional lisp），这种情况计算机语言设计者们怎么看？

++++

已经写了很长；再补充一些东西就是工业里有些目标没那么hefty的工具，即不去证明绝对的正确性，但仍然非常有用，比如静态代码检查工具，比如基于模型的code generation工具，现在几个mcu厂商的ide，都已经摒弃了让开发者coding每一行驱动的做法。如果文件分拆合理，有一部分文件就完全是gui工具和codegen控制的，图形界面上改改就产生代码，是巨大生产力提升而且也改善正确性，实际上包括很多并发同步量都是可以gui配置然后gen代码的。

++++

但实际上写了这么多，也没提到一个对这个话题而言非常重要的概念，什么是『正确』。Ayer的学生AC Grayling在剑桥的一个学院做过一个哲学报告，讲wittgenstein的；在介绍这个报告时，女院长表示自己对如何证明true非常感兴趣，因为她做了一辈子自然科学，都只知道false是可以证明的，true没法证明。

这个哲学问题在计算机程序上是有意义的。就象前面说的有限测例的测试方法，在没有遇到bug（或触发bug的场景出现）之前，当然没有人知道bug存在，而这不一定是因为其中一个程序员的粗心大意，还有可能是bug位于所有人加起来的认知之外。这是没有办法找到的bug，可能我们virtually只能承认，true，不过是not false yet。

先写这么多。有时间再补充点有意思的项目。

https://weibo.com/1655747731/N7Uil0z48?pagetype=groupfeed