1樓：
講道理，有時間看這種水文不如去看
Can programming be liberated from the von Neumann style? 老生常談了。
A Basis for a Mathematical Theory of Computation JMC 是幹啥的。
Computational Logic PX classical logic。
有點興趣讀下歷史書的可以看 Mechanizing Proof: Computing, Risk, and Trust
想換下口味的可以看看 Does APL Need a Type System?
建議這種沒搞明白 type theory 是幹什麼用的去好好看看 Simon Thompson 的 TTFP，順便去學下 Nuprl。還有就昰下次寫水文記得寫 ref 啊，不然只有電波男才看得懂要說什麼。
稍微認真看了下，還是發現了不得不吐的槽點，你 extract 出來的是 meta program 難道就不能算 program 了麼。
Coq, Nuprl 這樣的 proof assisted 使用的 dependent type theory 有足夠的表達力作為 meta theory，在裡面 reasoning 其它的 dependent type theory 都不在話下 (Coq 用來 formalized 了一部分基本了 Nuprl 的 Computational type theory，Nuprl 用來 formalize 了 Cubical type theory)，embed 乙個 propositional logic, first order logic 什麼的自然沒什麼問題，在用 type 作為 program 表示的時候 proof 成為 meta program 不是很正常的麼。我本以為有何高見，然而卻昰用原來立意可以很高的素材得出了這麼個 trivially 有問題的結論。這邊還有通過 embed classical logic 生成 sat solver 演算法的的呢。
Classical propositional decidability via Nuprl proof extraction
哪怕就是吹一下 supercompiler 和自動化證明的關係也行啊。
如何評價王垠新博文《那些垠黑們》？
現實世界裡，我的身邊充滿了敬佩和支援我的人。之前的公司 20 多個中中國人，大部分都直接或者間接看過我的文章，大部分人都喜歡我，支援我。只要我說要回國，有要挽留的，有要幫忙的 這裡面只有乙個人是不尊敬我的。這個人輪子吧? 我對垠神是路人，不黑不吹。有關注他的部落格，但只看技術類文章。我覺得垠神的目標...
如何評價王垠的博文《Google的眼光》？
仲毅 翻了下這個作者以前的文章，發現作者真是個谷歌狂魔，三句話不離自己在谷歌工作的經歷，看來還是太重視作為前谷歌員工給他帶來的光環。 已重置 說來說去，谷歌是做過錯事，但也在有些地方做的很不錯，對吧，谷歌手持整個網際網路霸權 搜尋和半個移動網際網路霸權 安卓，能連續兩次站在時代之巔，把握時代趨勢的企...
如何評價王垠最新博文《經驗和洞察力》？
CzJun 有一些話聽起來，因為習慣問題，最表面最初的心理反應會是感覺這話有點虛頭巴腦，但是，這話可能真的是句句是實實在在的事情。就像一塊板磚，實在，簡單，真實的存在著。這個文章是句句都是實實在在的。 yaoyao 王垠說的沒錯，洞察力才是如我這樣的人真正的價值之所在。經驗不值錢，是因為經驗是屬於過...