#公众号
公众号【工具艺术家】，每一期采访一位独立开发者，最新的一篇文章《对话开发者第29期：我们更在乎的是，到老了，回顾这贫困潦倒的一生，是否做了几件有意思的事？》。

#文章推荐
《野心与梦想：国产大飞机浮沉五十年》

由于毕业于北航的缘故，在我的同学里有不少（曾经）参与国产大飞机的研发工作。去年C919获得适航证，同学群里着实欢呼了一番。

外界对C919的质疑之一，就是这里的零件很多都是外包生产的，如何体现所谓自主研发的优势？我想时间拉长一些，过去我们只能给别人生产零件，如今慢慢地也能自己设计制造了。

引用文中的话来回答这个质疑：

“
争议也因此甚嚣尘上：核心零部件大多进口而来，到底能不能叫自主研发？

实际上，飞机能组装成功，就已经是一种顶级制造能力。

飞机制造本质上考验的是对几十万零部件进行选型、协调、管理的“系统集成能力”，以及整体设计规划和精密控制的水平。

做消费电子，把CPU内存硬盘等零部件往主板上一插，就是台能用的电脑；但造飞机，把发动机买回来装进飞机壳里——这玩意它飞不起来。

最重要的是，飞机组装也意味着零部件的自主采购权，带动的是整个产业链的进步。和消费电子不一样，“拼起来的飞机”本质上是一个供应链平台。
”

用发展的眼光看问题，而不是仅仅只看一个时间的截面得到一个静止的结论。小时候经常看到的一句话“几代人的努力”去做某件事请，长大了以后觉得这样的话并不是空话，在很多领域咱们落后，于是就需要几代人接力去逐步靠近这个目标。

#Databend
Databend是一款基于云原生的数据库，底层的数据存储都跑在各种云服务之上（AWS、阿里云、华为云、腾讯云，etc），于是就需要一个数据访问层（Data Access Layer）去屏蔽底层不同存储介质的差异。

一年多以前，团队内的小伙开始构思将这部分功能独立出来成一个单独的模块，这样也能方便其他有类似需求的项目，这个项目就是后来的OpenDAL。后来也确实有不少项目用到了这个库，包括：sccache、GreptimeDB、RisingWave等。

经过一年多的生长，最近OpenDAL项目进入Apache基金会的孵化器了。

#Rust
Rust死灵书（《The Rustonomicon》） 的 中文翻译版，翻译者应该在字节从事Rust基础架构工作。

#播客
《18. 商业口述史：从美国往事，到Google输掉Open AI第一局》
非常精彩的一期访谈节目，前半段嘉宾聊自己的求学、从业经历，后半段聊曾经就职的公司以及对AI的看法。

BTW：陆奇是怎么保持多年最早到公司、每天工作十几个小时的，短暂做到不难，常年如此非常难，很好奇。

#杂
聊一聊我做为一个数据库从业者对Chatgpt的看法。

本质上来说，Chatgpt这样的工具可以认为又是另一个“效率工具”。而程序员这个群体，可能是最会给自己造“效率工具”的群体，没有之一，比如：云计算、SAAS，等等的。换了其它创作类群体，比如画家、作家等等，他们更多的时候都只能等待别人给他们造效率工具来提升效率。这些不会自己造工具的群体，当看到新的效率工具出现时，都会被之震撼；而由于一直没有革自己的命，当真的变革来临时，很多人没有来得及转身就被替代了。

从这个意义上来说，做为程序员还是很幸福的：一直保持对自我的迭代、更新，就像我一直说的那样：“编程”是普通人类最容易拥有的“超人技能”，没有之一。

所以，什么“降本增效”、“革自己的命”这些说法，对程序员群体来说早已不陌生，相当一部分人的软件生意就是给另外一群做软件的人做工具。这次Chatgpt能如此出圈，我想更多的就是前面说的，给那些不会自己造效率工具的群体带来了惊喜：原来我只要说一些人话，这个工具就能来辅助我了，不需要我掌握更专精的工具（比如会编程）。

为什么最近几年，所谓的“独立开发者”越来越多被看到听到了？我想主要有两个原因：App Store、Steam这样对独立开发者友好的软件商店，极大得方便了开发者宣传产品、以及支付渠道的通畅；其次就是前面提到的这些面向开发者的效率工具、平台越来越多越来越好用了，不再需要开发者18般武艺样样精通，自己去维护一套服务、自己来运维服务器，这些细节已经由云计算厂商、SAAS公司给你做了，开发者只需要挑选合适的工具，自己做最核心的产品体验部分，这样就能搭积木一般把产品搭建起来。

软件行业里，这么多年一直在迭代各种类型的软件给程序员本身来提升效率：汇编语言到高级语言、简单的文本编辑器到专业的IDE、云平台、SAAS，等等。这不是第一次由程序员群体自己发起的效率革命，也当然不会是最后一次，这些迭代一直以来都在进行着，程序员们早就见怪不怪了。

从软件开发者的视角来看，这一点再自然不过：软件就是要屏蔽底层的实现细节，把方便留给上层的使用者。于是云计算屏蔽了底层的服务器、SAAS抽象出来通用的服务，等等。

回到数据库这个行业来，本质上“数据库”也是给开发者“降本增效”的软件之一。当“开发者”的门槛降低，意味着有更多的人可以通过和机器打交道的方式来工作。以往这个门槛相对较高，可能需要会一些编程语言，还需要系统学一些计算机的知识：算法、操作系统，等等；现在很多时候，可能只需要简单的SQL就能满足他们数据方面的一些增、删、改、查需求。从这个意义上来说，SQL确实是跟很伟大的发明，这是一门描述性的语言，又是“异构”的，完全不用在乎你底层是什么Python、Java还是CPP来实现的。对于复杂的SQL如果不会写，还能使用Chatgpt来辅助生成，比如Databend能够结合AI辅助生成一些SQL了：https://databend.rs/doc/sql-functions/ai-functions/ai-to-sql

我做为一个数据库的开发从业者，在开发者的门槛变低之后，反而是会更加乐观的：因为有更多的人需要我们提供的服务了。

#杂
以前看过一个关于钱和人生的比喻，大概是这么说的：假如人生是一场自驾旅游，赚钱就是给这场自驾旅游加油，没有油车就走不远，旅行就无从谈起了，但是大概不会有人会把去各个地方加油当成这场旅游的目的。

这是我看到关于钱和人生关系最好的一段描述，赚钱到底是目的还是手段，这只有自己才能想明白了。

对我来说，人生短短几十年，尽可能找到自己喜欢做的事情，多做点自己觉得有意义的事情，如果能顺便赚点钱过上舒适的生活，那就更好了。不排除有些时候，世俗的压力得向生活低头做些自己并不喜欢的事情，但这跟上面这句话也并不冲突。

我看到很多人，即便在我的认知里已经有不少钱了，但是仍然会为了赚钱做一些吃相难看的事情，这可能就是太想明白钱到底是目的和还是手段。赚钱是为了让你过上体面的生活，生活体面了之后人也应该“体面”起来，而不是反之最后变成了它的奴隶。

#杂
以前工作里遇到的问题：某业务服务器有内存泄露，一时半会儿解决不了。于是在前面加了一组网关服务器，每个网关维护后面的一组业务服务器列表，负责无脑转发客户端请求，以及在失败的情况下转发给另外的业务服务器处理请求。

这样改动之后，业务服务器可以定期重启，重启时通知网关从服务器列表中删除，不再向这台业务服务器转发请求，重启完成之后，业务服务器再通知网关重新加入服务器组对外提供服务。

“计算机科学领域的任何问题都可以通过增加一个间接的中间层来解决。”

#杂
关于数学学习，有两个观察：

* 即便一个人的数学知识储备到了高中数学层次，部分小学数学的奥赛题也不一定能解得出来；
* “鸡兔同笼” 是非常经典的小学数学奥赛题型，可是如果学到了初中数学，有了未知数、方程式的概念，这个问题就是非常简单的解二元一次方程。

这两个观察的思考是，过度在技巧中沉浸，很多时候意义不大，因为”技巧“的钻研是个无底洞；与此相对的是，很多问题当你掌握了更高级的工具之后（比如上面的二元一次方程之于鸡兔同笼问题）就能马上迎刃而解。

所以对大部分人来说，掌握了一门知识的基础概念、做了一定量的练习之后，就可以接着去追求往更高层次的知识，而不是过度沉浸在”技巧“中。如何判断对一个知识的掌握已经“足够”了，首先根据二八原则来，掌握最常用的八，其它的边做边学；其次，如果有这个领域的经典教程，那么编撰这套教材的人肯定在这个领域已经浸淫多年，书里的重点、练习做得差不多就好了。

把这个观察得到的方法论推而广之：很多时候我们关注于“解题”本身，慢慢得过于关注技巧、为鸡毛蒜皮的问题解决而沾沾自喜，以至于忘了往更高的层次去走。比如以前还在写C的时候，经常为解决某个内存引发的问题而沾沾自喜，这些问题放到Rust语言的设计里编译器就不会让这种情况出现，很多问题在用了另外的角度、有了别的视野、换了其它工具之后就不复存在了。

人生苦短，别把太多问题放在“解题技巧”上，很可能当视野打开之后，问题就不再是问题了。解题之前，不妨多问自己几个问题：这个问题非要解决吗，能不能换别的路线绕开它，有没有更好的工具辅助解决这个问题，下一次能不能避免出现类似的问题，等等。扁鹊三兄弟的故事里，扁鹊就是兄弟里最能解题的人，而他两个哥哥都能问题发生之前避免问题，所以他们能力更强。

最后，反过来看前几年出台政策把奥赛的热度打下来，我认为是有可取之处的。如前面的讨论，奥赛过度关注技巧，这可能也是中国为什么赢得这么多奥赛金牌却出不来几个知名数学家的原因之一：解题解到最后，并不能让你成为一个大家。

#播客
最近新出的一档程序员主播的播客节目 《硬地骇客》 ，《从个人兴趣到财务自由：独立开发者也可以这样做开源》 这一期专门聊了几个商业化做的不错的开源项目，我这才知道 Dracula 做为一个编辑器主题还能这么赚钱。

最后谈到的由HomeBrew作者发起的 https://tea.xyz/ ，这个专门针对开源项目的web3项目也很有意思。

#杂
我现在算是对Sqlite运行机制有一些了解了，想围绕着它的生态在此之上做一些个人项目，但是这个数据库产品是在C端被用得更多，而我的工作方向在后端，所以有没有平时用Sqlite的人能说说它用起来有哪些不太爽可以改进的地方，或者是它的相关工具（比如数据恢复、中文搜索功能），谢谢。

#杂
二八定律最伟大的地方，是告诉我们很多时候，世界运行的规律是“非线性”的：

* 可能努力了几年，前面几年基本没啥回报，到了第五年开始爆发性的收割；
* 工资的增长和工作年限没啥关系，也就是说不一定每年涨个10%，可能是前几年不怎么涨，积累够了一个跳槽就翻倍了。

等等。

经常看到一个词“学生思维”，就我个人的体会，学生思维里常见的误区就是认为这个世界是“线性”的，比如认为努力就一定有回报，这可能跟学生在学校的“反馈”环境很有关系：去解决有标准答案、且指定范围的问题。离开了学校之后，面对的很多都是开放性的、没有标准答案的问题，于是二八定理告诉你，努力不一定马上有回报，或者说回报不一定马上能看得见。

成年人的世界里也不是完全没有线性反馈的事情了：锻炼就是一件能线性反馈的事情。能有线性反馈的事情，相对来说都是“容易”的：只管去做，做的过程中一直有反馈，得到的正反馈又能马上推进你继续做这件事情，而做非线性的事情就更加考验人，这可能也是很多成年人会喜欢朋友圈里发健身图的原因之一吧。

这周日（4.16）晚上八点，飞书群线上沙龙：Databend ｜ Rust编译优化小技巧，大家不见不散

#数学
圆周率π是最常见的两个无理数之一（另外一个是自然常数e），数学上已经对这些无理数的意义做了充分的解释。《疑犯追踪》S02E11中男主对π的解读是最浪漫的：

Student Girl: My Friend Has A Question, Mr. Swift . “What Is Any Of This Good For, And When Would We Ever Use It?”

(The Class Laughs.)

Finch : Let Me Show You. Π. The Ratio Of The Circumference Of A Circle To Its Diameter . And This Is Just The Beginning. It Keeps On Going. Forever. Without Ever Repeating. Which Means That Contained Within This String Of Decimals Is Every Single Other Number. Your Birth Date, Combination To Your Locker , Your Social Security Number. It’s All In There Somewhere. And If You Convert These Decimals Into Letters, You Would Have Every Word That Ever Existed In Every Possible Combination. The First Syllable You Spoke As A Baby, The Name Of Your Latest Crush , Your Entire Life Story From Beginning To End. Everything We Ever Say Or Do, All Of The World’s Infinite Possibilities Rest Within This One Simple Circle . Now What You Do With That Information, What It’s Good For, Well, That Would Be Up To You.

“Pi 一个圆的周长与它的直径的比，但不仅是这些而已，还有更多，永无止境，毫无重复。小数点后的这一串数字，每一个都是单一个体，你的生日、寄物柜锁密码、社会保险号码，都在这一串数字某处。如果你把这些数字转换成字母，你会得到每一个词，在每一个可能的组合中出现，你婴孩时开口讲的第一个音节、你心上人的名字、你从头至尾整个人生的故事、所有我们说的话和做的事…这个世界所有无尽的，可能性都在这个简单的圆里。你拿这些信息做什么…有什么用处…全都取决于你。”

B站上截取出来这一集的相关视频。

补充信息：但是π目前并没有证明是一个正规数（Normal Number），即数字显示出随机分布，且每个数字出现机会均等的实数，也就是说：虽然π是个无理数，但是也不能保证任意数字一定会出现在这个无理数的数字序列里。

#Databend
Databend最近搞了一个side project：AskBend。

这个项目依赖于Databend Cloud来存储Databend官网的文档数据，喂给OpenAI之后，生成一个可以根据文档内容回答问题的“客服机器人”。这个项目本身也开源了：https://github.com/datafuselabs/askbend，我的另一位同事把项目用在了自己的博客上：https://ask.xuanwo.io/，可以看到效果也不差。

另外今天看到一篇文章，有同学参考这个项目给PG也加了类似功能：https://al-assad.github.io/posts/replicate-askbend-on-postgres/

我开始在想：给sqlite做一个类似功能，好像也不赖吧，毕竟我最近也在找可以做的sqlite周边生态产品。


Reference：
* https://t.me/codedump_notes/429

#Databend
从2021年初成立公司到今天，经过两年多的打磨，Databend Cloud终于要在2023年4月20日这天 官宣发布 了。

#剧
去年无意间看到的一部剧 《破事精英》 ，情景喜剧类节目，剧情设定是一个公司里最不起眼、各种破事的“破事部”发生的故事，讨论了很多职场话题：PUA、中年危机、职场性骚扰等，当时看的时候抱着60分就好纯打发时间的念头去看，实际追完觉得能有个75分。里面甚至有个工作机器人起名叫“盯盯乐”，要是这部剧是阿里旗下优酷出的话，那效果能拉满了，属于去年看过的剧里最为惊喜的一部，眼看着 第二季 就要出来了。

#杂
《A Tutorial Introduction to the Lambda Calculus》，关于lambda演算的一个简明教程，只有17页。

#类型系统
#书单
微博上一位老兄列举了一堆学习类型系统的书，我转抄来电报，给每本书加上了豆瓣页面跳转，原微博地址：https://weibo.com/1683375645/Kk7Vr5yrr


整理一下关于类型系统的书籍。

Benjamin Pierce - Types and Programming Languages，是最好读的一本
Benjamin Pierce - Advanced Topics in Types and Programming Languages，这本写的比较散，不系统，但设计大量现代类型理论的课题

Hindley and Seldin - Lambda-Calculus and Combinators
Hindley - Basic Simple Type Theory

Hindley的第一本，应该是写给数学背景不错的计算机科学专业的学生的，非常系统的处理了几个有类型的λ系统；第二本则不是象它的题目所示，是关于Simple Typed Lambda的一般性理论，而是特别处理了一个Simple Typed Lambda系统，这个对深入学习Simple Typed Lambda系统的人来说是应该看的；

Barendregt - Introduction to Lambda Calculus
Barendregt - Lambda Calculus with Types

Barendregt差不多是Lambda领域最高学术权威。这两本书极其吃力，第一本和计算科学或者计算理论均无关，是纯数学，研究(untyped) lambda系统本身的特性（terms modulo convertibility），这本书的prerequisite比较恐怖，需要数理逻辑，集合论，拓扑，抽象代数，范畴；内容范围和Hindley的Lambda那本基本一致，但是烧死的脑细胞比Hindley那本多很多倍。

Barendregt的第二本是Typed Lambda，这个跟类型系统关系比较紧密一些；这本和第一本的关系不大，但有不少提到的地方。

Negerpelt and Geuvers - Type Theory and Formal Proof

这本也是数学专业的，但不是那么刚；而且它和证明论建立联系，应该是搞定理证明或者（类型系统）程序证明的人应该读的；比Hindley和Barendregt的书都好读而且内容更新；两个作者之一是Barendregt的学生。

Harper - Type Systems for Programming Languages
Harper - Practical Foundations for Programming Languages

Harper是卡梅的PLT权威，第一本不是书，介于一个Lecture Note和一个没写成书的草稿之间；第二本基本上是属于计算机科学领域的最刚的关于类型系统的介绍了，相当全面，但显然不会有数学书那么要求高了；这本应该算plt方面的最好教材。

++++

前面都是搞理论的，这里有几个可以实操的，是程序员们喜欢的方式。

Friedman and Christainsen - The Little Typer

这几天它我正在看这本书，是一本奇书；它实际上是在讲现代类型理论（Modern Type Theory，Martin Lof/Intuitionistic Type Theory，CICp in Coq, Luo's UTT, HoTT etc）中的一个特别的topic，叫Dependent Type的；简单的说Dependent Types允许你定义依赖于值的类型，但是定义的方式，在编程语言实现时，也是用操作值的代码实现的，而不是象例如C++的metaprogramming或者其他语言的generics一样使用另一套语法和操作符。

The Little Types构建了一个教学用的小语言，Pie；这个语言基于Racket平台，基本上你如果是搞语言研究，在开放平台上，Racket和Haskell是最多的选择，魔改ML也是个办法。学习Racket(Scheme)对于愿意花时间折腾语言的人来说应该是值得的，Racket有一套自己拓展语言的很好的框架和文档。

Stump - Verified Functional Programming in Agda

这是以Agda语言为例讲解在Agda里如何书写证明程序的，Agda也是General Purpose语言，但是很弱，就是不能实际开发应用。

Mimram - Program = Proof

这本也是讲了Agda的，但是只占其中一章；前半部分都是在讲基础知识，数理逻辑，Typed Lambda等，最后还有介绍HoTT的。

Brady - Type Driven Development with Idris

Edwin Brady是Idris语言的发明人，这个语言也是使用现代类型系统的（Luo's UTT），Idris是目前我知道的完全支持Dependent Type的语言里最Practical的一个，但仍然只是玩具级，开发不了复杂应用，但裸io和网络通讯还是有的，我看到Brady有论文写Web开发的。

++++

去Youtube上搜索Dependent Type，能找到Haskell社区开发者做的语言插件，还有Christainsen讲他的Pie；都有令人震撼的例子。

++++

我的桌面上还有一本四哥推荐的奇书：

Stepanov and Rose - From Mathematics to Generic Programming

书的作者是C++ STL类库的核心开发者；C++的Template实际上是一个图灵完备的系统，只是只能在Compile Time运行。它能做很多的事，但是做得非常困难。

C++没有前面说得这些现代类型系统，它是古早的nominal (or nominative) type system，当然很多新语言也仍然使用这个类型系统，包括Dart, Swift, Kotlin, Rust等等，但也有向未来迈进的，例如TypeScript就选择了Structural Type System（被Erik Meijer盛赞），还有Go这种奇葩的Duck Typing，你不知道未来会进化到哪里去，还有那么多的脚本语言，你也不知道是不是哪天哪些头脑发热的年轻程序员就给它们武装上一个现代类型系统。

换句话说，Stepanov的高超技巧，未来会在支持现代类型系统的编程语言里更容易实现，『飞向寻常百姓家』。

++++

在reddit/quora等社交网站上有很多关于现代类型系统的编程收益，以及它是一个大大的进步，还是和以前的类型系统进化一样，只解决了少少的问题但难度却陡增，有很多有益的讨论。

主流的观点和今天 @Puzzler_红叶 在另一个帖子里的回复一样，就是基于证明论和类型系统的语法方法，不如基于模型论的模型检查和模型验证方法；原因是后者的适用性更好。

++++

但我有不同的看法，我认为基于现代类型系统的编程语言将不可避免的进入产业，不但大流行，而且会产生深远的影响，只是这个时间不会太快，结果也未必太好，而已。原因如下：

1 类型系统是当前程序开发者的技能树中的东西，只要语言工具做得够好，应用并不是问题；而基于Model Checking技术写Spec完全跑到另一个Domain去了，除非老板安排，开发者没法支付去学习这个领域的知识的成本，也缺乏普适性。

2 在类型系统中进行数据合规/协议合规要求，是产业非常需要的东西，Idris语言作者给出的很多例子，开发者都看得懂而且很明确的知道，I need it；这样只要门槛不太高大家会去尝试和使用的。

3

象Haskell那样把很多数据结构塞进类型，还有要了老命的monad和do notation，不管开发者怎么吹捧，我都坚持认为是这些东西把Haskell语言给『毒』死了。

我用web技术打一个不算很恰当的比喻，web页面是三个东西构成的，html的layout，css的样式，操作dom的javascript实现交互和数据处理；如果设计者是个很嚼性的人，比如它坚持认为有脚本语言就够了，样式问题可以搞个像素系统，canvas，这web还能象今天这样流行吗？或者这个设计者是css大师，说不需要复杂脚本语言，交互都用css来搞定，它当然是『能』的，但问题是还有几个人愿意跟你一起『能』呢？

对吧。编程语言就象Web技术一样，要坚持多元化，Pluralism，要选择最恰当的技术解决它最擅长解决的问题。类型和证明当然不是包治百病，但是现代类型系统叠加函数式编程，它能向前进很大一步，让开发者觉得学习函数式编程和类型系统带来的工程收益是划算的，有一种还算符合直觉的方式可以编写程序的Constraint。

至于什么是并发的最佳原语，应该怎样在mutable/immutable之间找到平衡让数据结构即富有效率又不是过于抽象，那并不是类型系统要去回答的问题。那也许是通过其他技术来解决，使用其他理论。

基于以上的判断，我的理解是在可见的未来，不会很近但是也不会很遥远，现代类型理论的成果会深远影响编程语言；年轻的计算机专业毕业生会学会Agda/Coq这样的东西走出校门；知乎上貌似有人说waterloo给计算机专业本科生开了coq的课程，据说结果惨烈，哈哈哈，但是我相信老师们会进化的；最终这些努力都会转换成产业里更好的软件质量和更高的开发效率。

通过更好的类型系统解决更多的软件质量问题，是在过去三十多年的产业里梦寐以求的东西，因为缺乏良好的数学基础，只能催生出大量的工程技术解决问题；当然类型系统不是一帖灵，但是它肯定可以把软件质量，或者说程序员们能应对的系统复杂度，推到一个全新的高度。

#type theory# #type system# #dependent type#