我就比较好奇那个形式化验证到底做到了什么程度。其他无感，反正我大概是不会用⋯⋯
论坛有没有华为的内部人员聊一聊形式化验证 
生态的话其实只要愿意破坏市场规则都可以很快起来。
有道理。想起来大学的时候听说过一件事情，华为为了节约资金到处在找国内可以生产机器外壳的厂商，然后随着国内工艺的提升终于找到了。结果后来发现喷漆工艺国内还是不行，后来又去国外喷漆了。 所以鸿蒙系统要想牛批起来，就必须要多个公司，部门之间相互配合才可以。
1 个赞
鸿蒙只是一个引子， 不管它现在有多烂，只要华为能抓住这个舆论的东风，借势而行，它就会发展起来，代码烂可以改嘛。
5 个赞
一个东西长得像Android，用起来像Android，那它就是 Android
鸭子:没错,正是在下!
1 个赞
这个只能说像Android，不能说是。。。。。
一个东西长得像电视，用起来像电视，但其实它是智慧屏
1 个赞
据说是形式化证明微内核的bug-free（因为内核很小）。道听途说的。
华为这个事情让我想到了 systemd 的发展， 当时 systemd 在发展初期的时候，得到了广泛的支持，没几年已经发展成庞然大物了。
智慧屏幕用起来不像电视吧？要不然怎么叫智慧？
不要忘了 TEE 可以和安卓并行运行：
是的，systemd 并不符合 Linux 哲学，只是由于大厂商的支持发展也很好。尽管现在我依然认为很烂，但是大家都用也没办法啊
linux没有哲学啊，有哲学的那是unix。。
1 个赞
有谁普及一下形式化验证
普及形式化验证？很多人连 Haskell 都学不好，连TDD都做不好，还指望普及形式化验证？如果你是指科普一下，那只要理解 Curry–Howard isomorphism 和 Computational trinitarianism 就行了。
所以Haskell和TDD和形式化验证又有多大关系？
Haskell是没有dependent type的，TDD和形式化验证完全是两种思路
1 个赞
什么关系？智力要求递进的关系。
还是你觉得连Haskell和TDD都学不会的人群也能普及形式化验证？
没个精通 CL + ML 三十年，连个 NuPRL 都不会装，还好意思在这讲形式化证明？
) 狗头
没听说过用 NuPRL 形式化验证的 OS Kernel ，介绍几个？