这两个太丟人了，外行都不如。我个 hobbist 都知道 IOKit。
就我个人的读yin技巧，yin的意思全在开头那个链接到模仿lisp machine设计的思路的文章里，剩下的基本可以当屁话。 
1 个赞
我看的时候就想“这不是lisp machine吗”www
好吧好吧，已经听不懂了，占楼留个mark，提醒自己可以不用往下翻了，你不懂 
层主那个例子感觉看不出什么东西，因为这个main函数本质是纯的。。。
如果能有修改全局变量的非纯函数就好了。
我说了全局变量是简单粗暴直接禁止的
问题是：如果有一段程序（使用C语言）里使用了全局变量怎么办？
使用clightgen转换那段程序，会产生什么？
是否会变成一个输入一个状态返回一个状态的函数？
对嵌套结构里的成员进行更新，会产生像lens那样代码吗？
对同一个变量连续赋值呢？（自动变成函数compose做组合transform？）
我理解的 CompCert 是允许副作用的。关于全局变量可以看 VST 里面用到的例子 global.c 和对应的用 clightgen 得到的 global.v。我觉得文档里这张图说的只是把副作用从表达式中抽取出来，而不是说消除副作用。
华为做了一件”牛逼”的产品，有的人专注于把它变得更牛逼，有的人执着于”你怎么证明它就是牛逼”?
我很好奇，安卓刚出来的时候都做了啥验证吗?
就只能手改成函数传参。编译器没有这么聪明，不支持的特性全部要手改。
lens 是因为 Haskell 沒有 linear type 才搞的，能 destructive update 的用不着 lens。
这没有全局变量，只有常量。也就是说，全局“变量”要保证不能被修改才能转化。
确实这里都是常量，没仔细看。不过我试了一下用 clightgen 编译下面这段代码，看起来还是能改全局变量的：
int g = 1;
int h(void) {
g += 1;
return g;
}
int main(void) {
int y;
y = h();
return y;
}
生成的 Coq 中的主要部分是：
Definition v_g := {|
gvar_info := tint;
gvar_init := (Init_int32 (Int.repr 1) :: nil);
gvar_readonly := false;
gvar_volatile := false
|}.
Definition f_h := {|
fn_return := tint;
fn_callconv := cc_default;
fn_params := nil;
fn_vars := nil;
fn_temps := ((_t'2, tint) :: (_t'1, tint) :: nil);
fn_body :=
(Ssequence
(Ssequence
(Sset _t'2 (Evar _g tint))
(Sassign (Evar _g tint)
(Ebinop Oadd (Etempvar _t'2 tint) (Econst_int (Int.repr 1) tint) tint)))
(Ssequence
(Sset _t'1 (Evar _g tint))
(Sreturn (Some (Etempvar _t'1 tint)))))
|}.
Definition f_main := {|
fn_return := tint;
fn_callconv := cc_default;
fn_params := nil;
fn_vars := nil;
fn_temps := ((_y, tint) :: (_t'1, tint) :: nil);
fn_body :=
(Ssequence
(Ssequence
(Ssequence
(Scall (Some _t'1) (Evar _h (Tfunction Tnil tint cc_default)) nil)
(Sset _y (Etempvar _t'1 tint)))
(Sreturn (Some (Etempvar _y tint))))
(Sreturn (Some (Econst_int (Int.repr 0) tint))))
|}.
只是把副作用从表达式中抽取出来，而不是说消除副作用。
我一开始是想说这个意思。不过确实看图瞎猜不太好 
我给的这个例子确实没有全局变量,我这个只是展示了表达式中的side-effect.
开源了，会像当年 linux 一样吸引大量的开发者吗？
小声点，说好的11月开源呢 留点面子给牢厂。
现在好像说明年什么时候开源
挖个坟 就技术来说，鸿蒙OS到底是个什么层面的东西，现在有答案了，楼上的各位都想多了