就技术来说,鸿蒙OS到底是个什么层面的东西?


#22

我就比较好奇那个形式化验证到底做到了什么程度。其他无感,反正我大概是不会用⋯⋯


#23

论坛有没有华为的内部人员聊一聊形式化验证 :rofl:


#24

生态的话其实只要愿意破坏市场规则都可以很快起来。


#25

有道理。想起来大学的时候听说过一件事情,华为为了节约资金到处在找国内可以生产机器外壳的厂商,然后随着国内工艺的提升终于找到了。结果后来发现喷漆工艺国内还是不行,后来又去国外喷漆了。 所以鸿蒙系统要想牛批起来,就必须要多个公司,部门之间相互配合才可以。


#26

鸿蒙只是一个引子, 不管它现在有多烂,只要华为能抓住这个舆论的东风,借势而行,它就会发展起来,代码烂可以改嘛。


#27

一个东西长得像Android,用起来像Android,那它就是 Android
鸭子:没错,正是在下!


#28

这个只能说像Android,不能说是。。。。。


#29

一个东西长得像电视,用起来像电视,但其实它是智慧屏


#30

据说是形式化证明微内核的bug-free(因为内核很小)。道听途说的。


#31

华为这个事情让我想到了 systemd 的发展, 当时 systemd 在发展初期的时候,得到了广泛的支持,没几年已经发展成庞然大物了。


#32

智慧屏幕用起来不像电视吧?要不然怎么叫智慧?


#33

不要忘了 TEE 可以和安卓并行运行:


#34

是的,systemd 并不符合 Linux 哲学,只是由于大厂商的支持发展也很好。尽管现在我依然认为很烂,但是大家都用也没办法啊


#35

linux没有哲学啊,有哲学的那是unix。。


#36

有谁普及一下形式化验证


#38

普及形式化验证?很多人连 Haskell 都学不好,连TDD都做不好,还指望普及形式化验证?如果你是指科普一下,那只要理解 Curry–Howard isomorphismComputational trinitarianism 就行了。


#39

所以Haskell和TDD和形式化验证又有多大关系?

Haskell是没有dependent type的,TDD和形式化验证完全是两种思路


#40

什么关系?智力要求递进的关系。

还是你觉得连Haskell和TDD都学不会的人群也能普及形式化验证?


#41

没个精通 CL + ML 三十年,连个 NuPRL 都不会装,还好意思在这讲形式化证明?

) 狗头


#42

没听说过用 NuPRL 形式化验证的 OS Kernel ,介绍几个?