如何評價 HarmonyOS 鴻蒙系統的技術設計？
相關問題：
如何看待華為 2019 年 8 月 9 日正式發布的 HarmonyOS 鴻蒙系統？?www.zhihu.com因為那個問題下通稿太多了所以多提一個技術向的問題，希望大家不要流於表面講空話，盡量只關注技術細節，謝謝
據發布會稱是經過形式驗證的操作系統（不知道是驗證了整個內核還是部分組件..），很厲害了。
DeepSpec / FLINT@YALE 有一個形式驗證的操作系統項目 CertiKOS，是完全被形式驗證的的操作系統，甚至連使用的 C 編譯器都是經過形式驗證的 CompCert，介紹上說是「the first proof of functional correctness of a complete, general-purpose concurrent OS kernel with fine-grained locking」，這個項目絕對是突破性的。
但是可以商業使用的操作系統驗證成本應該會高很多，一個完全經形式驗證的系統可以做到在這一層次上沒有 bug 和安全漏洞以及抵抗攻擊（因為你依然可以用 side channel attack 之類的強行攻擊233），DeepSpec 就在試圖構建一系列經形式驗證的系統軟體 / 工具集。
具體內容還是期待開源吧，另外發布會真的很尬，就不怕內行反感么...
我只是一個希望以後能做 verification 相關內容的萌新，有錯誤歡迎指出~
p.s. 據可靠消息是用 Coq 做的，和 CertiKOS 一樣呃
謝邀，其實我只是個煉丹師，對 OS 方向的前沿了解比較少……因為興趣原因稍稍關注了下 verification 這塊。
在這之前，對 kernel 的 verification 有一個 seL4。seL4 也是一個 micro kernel，kernel 源碼大概 1.2w 行，整體是一個比較初級比較簡單的實現。（作為對比，linux kernel 4.9 有約 2200w 行代碼。當然 micro kernel 和 monolithic kernel 比規模並不是很公平。）雖然鴻蒙是個新 kernel 規模肯定沒有 linux kernel 那麼大，但是作為一個商業公司的產品級 codebase 肯定比 seL4 複雜得多。作為第一個商業 OS 的 verification，在學術界和工業界肯定都會引起巨大的反響。
目前還不清楚鴻蒙的 verification 是不是只包括 kernel，但是 OS 層面的 verification 肯定還是離真正的 bug-free 有一段距離，畢竟在 OS 之上就有 fs、lib 之類的東西可能引發 bug。順帶一提，和華為關係密切的交大 IPADS 實驗室在今年 SOSP 上發表了全世界第一篇 file system 的 verification paper，所以鴻蒙說不定不僅有 kernel verification，還可能會有 file system verification……
鴻蒙的內核沒有源代碼，不過lite os是2015年就開源的，可以看一下：
LiteOS/LiteOS?github.com
按照我看到的圖片，華為的鴻蒙os現階段是用了三個內核的：linux、鴻蒙、liteos，未來會把驅動剝離出來，只剩下鴻蒙內核。
也就是說，在我的理解下，這就是一個EMUI+鴻蒙內核+liteos內核的混合物，實質上應該還是個linux based emui或者說android based emui。
只有等內核完全替換成鴻蒙內核，這個鴻蒙os才能算是「獨立自主的內核」。
如果說目前的看點，就是「方舟runtime」、「分散式軟匯流排」和「鴻蒙內核」。
方舟runtime可以提高效率，這個有大佬講過。
如何評價華為的方舟編譯器？?www.zhihu.com
具體情況我也沒得驗證，不過這個原理講的看起來像是成立的樣子。
「分散式軟匯流排」，確實可能會容易的把所有設備的各種資源共享，這個大家也舉例子了：把手機攝像頭、電視攝像頭和未來華為筆記本的cpu、gpu等通過軟匯流排聯繫起來——但是目前還沒弄清楚這有什麼實際的好處，因為暫時沒看到這些和smb（共享文件）webcam之類的共享方式有什麼實質區別，也沒看到這種用處。
如果需要攝像頭，為什麼不直接在電視上弄一個？如果需要存儲，smb的共享優化一下通用性更好，macos就是現成的例子。總的來說，還看不出這種分散式有啥實際提升。
至於鴻蒙內核，沒開源的東西，不好評價。如果兩年內完全過渡到鴻蒙內核，這也勉強不算鬧劇——假如鴻蒙內核自始至終就基本沒有什麼作用，那這真的是徹底的鬧劇了。
我唯一感興趣的是經過「形式化驗證」的系統，因為這個在我們專業領域是個難點，除了個別軍工航天航空類軟體，其他很少有這麼搞的，希望不是吹的，這個你瞞得過消費者瞞不過內行。
至於其他的部分：
1，就發布個「膠片」，連繫統最起碼的demo演示都沒有，怎麼評價？技術設計？評價他們羅列以及編造的名詞嗎？
2，一聽到是分散式OS的時候就懶得往下看了，一群賣手機的忽悠消費者還行。。。誠不欺我，有分散式操作系統這個概念嗎？分散式系統倒是好幾十年了，分散式定義第一句話是什麼？就一終端系統你給我整個分散式架構，求求你嚴謹點，尊重這個行業。
3，一看到拿出表格對比「A家」「G家」各種暗示就覺得噁心，跟什麼公司學的？我從來沒見過Google I/O 上會出現類似的東西，可能這就是所謂的格局不一樣。
4，一說微內核我首先想到的是前不久關注的 Fuchsia OS的 Zircon，這貨早就開源了，但是 Fuchsia 一直低調得很。所以不知道他們有什麼關係，這個等著以後慢慢研究。
5，啥玩意兒沒有先聲明開源了，情懷先撂在這裡，真是奇葩。
我真的很好奇搞技術的你們怎麼看？就像樓上某位朋友說的，看的不尷尬嗎
在學界都是很新的東西直接拿出來商用還真的僅此一家。
到最後我也沒看出來怎麼個distributed法，不過distributed至少是有用的，比如智能家居，把你家的所有華為設備統一成一個分散式系統的話，還是挺有趣的。(但如果這玩意真到了能商用的地步，某plan 9早統一地球了(不過最近plan 9已經通過某種方式變相統一地球了))
所以華為這次把實驗室里都還沒做出來的東西直接拿出來商用，不怕翻車的么。
推薦閱讀：
TAG:操作系統 | 華為 | 鴻蒙HarmonyOS | LiteOSIDE |