所以 Nim 就是所谓的 jack of all trades (but master of none)。
Idris 和其他类似设计的编程语言的问题是，我现在认为 Type Driven Development 是伪需求
对啊
这里同时还有一个国内计算机本科常有的误解，GCC 之前已经有很多 C 编译器了，第一版 GCC 就是纯 C 写的，没用一行汇编。
显然同理，第一个 Common Lisp 直接用现成的其他 Lisp 实现改改就有了。后面的CL实现就可以用CL写了。
归根结底/有始有终/照葫芦画瓢(意淫), 最底层还是用C的吧?我猜是用C实现了最基本的Lisp语法, 例如 if关键字和括号断背山(打错字了)语法, 再用这些实现好的Lisp去实现"官方"的 CL-USER 函数/宏 (源码里有)
你自己数下这些 C 文件的行数。完全不够实现一个最简单的 lisp。内容也没一个和 lisp 实现有关的，其实都是些无关紧要的功能，比如从操作系统获得时间。SBCL 是可以直接生成汇编的。
你这就和看到 GCC 源码树里有汇编就以为 GCC 用汇编写的是一样的错误。
你编译SBCL的时候没读过说明吗，编译需要一个现成的SBCL，或者其它 CL 比如 CCL。
;; Warning: according to upstream, CCL is not bootstrappable.
;; See https://github.com/Clozure/ccl/issues/222 from 2019-09-02:
;;
;; "As far as I know, there is no way to build CCL without an existing
;; running CCL image. It was bootstrapped back in 1986 or so as
;; Macintosh Common Lisp, by Gary Byers, I believe, who is no longer on
;; the planet to tell us the story. It SHOULD be possible to port the
;; CCL compiler to portable Common Lisp, so that ANY lisp could build
;; it, as is the case for SBCL, but I know of no attempt to do so."
摘自 Guix 仓库
Another note in build recipe of SBCL
;; From INSTALL:
;; Supported build hosts are:
;; SBCL
;; CMUCL
;; CCL (formerly known as OpenMCL)
;; ABCL (recent versions only)
;; CLISP (only some versions: 2.44.1 is OK, 2.47 is not)
;; XCL
;;
;; From NEWS:
;; * build enhancement: new host quirks mechanism, support for building under
;; ABCL and ECL (as well as CCL, CMUCL, CLISP and SBCL itself)
;;
;; CCL is not bootstrappable so it won't do. CLISP 2.49 seems to work.
;; ECL too. As of 2020-07-01, ECL was last updated in 2020 while CLISP
;; was last updated in 2010, and both take about the same time to build SBCL.
;;
;; For now we stick to CLISP for all systems. We keep the `match' here
;; to make it easier to change the host compiler for various
;; architectures. Consider switching to ECL if it gets faster than CLISP
;; (maybe post 2020 release).
SBCL 和 CCL 都需要 Lisp 实现来编译
听君一席言胜读十年书
看来SBCL的宝贵的源代码我是迟早要去认真看看的 (很多财富就是因为免费/开源的所以我们觉得不宝贵)
吾先去Google一下"Lisp实现"本质是什么(吾原以为就是用C语言写的基本/底层解释器)
Nim 是太兼容并蓄了，代码质量不高。
TypeDD 有没有需求不知道，能写完编译通过就没 bug 的需求还是非常有的😄
那不好意思，现在的编程语言都做不到。甚至最fundamental的问题，一开始需求都搞错了，编译器再强也没有用
玩 Haskell、Scala 的人都这么吹的呢😂
现在有很多研究性质的编程语言，试图在编程语言里融入尽可能多的形式证明，写代码时就已经证明了代码没有 bug，希望这些能有大发展。
Ada 那个 Spark 变体可能是这方面目前最成功的。
别杠，人下的指令错了，程序也没能力纠正😄
能把内存错误、并发错误、类型错误、不完备的分支、前置条件后置条件的证明都解决掉的话，已经是个巨大进步了。
六七十年代 Dijkstra 推广 structured programming 的时候就在教怎么给代码做形式化证明了，放现在几乎是个程序员都知道goto有害，然而能给自己代码在纸上写证明的恐怕10%都没有，实际上纸上写不出来的话，用程序辅助也很难有啥帮助。我为啥说 TDD 是伪需求，就是因为有能的程序员不稀罕些，TDD 能做的验证他们在纸上用 hoare triple 也能做。他们提倡的是 correct by construction，写下代码之前就能保证得到正确的结果，剩下的也就是 typo 这样小错。这样做也不用什么特殊的编程语言，C，Pascal，Lisp，Haskell 都能用 CbC 的方法。
我说的“连需求都没搞对”，就是形式化验证最为重要的 specification problem。就目前来看，程序员水平不够高，是不能推广形式化的主要问题。所谓的研究性质的编程语言，也都没有做到傻瓜式操作的地步。
1 个赞
还是联想到自己的老话：抽象好，尽力让自己的加减法进化成乘除法，十几年后再进化到指数对数（几十年后再复数）
TDD 不是为了形式化证明吧，TDD 是为了写的代码达到了设想的效果。重点是后面的 DD
TDD需要集成其他技术（e.g. synthesis）才能体现威力。
理想的情况下，程序员日常应该是这样的：
-
使用 AI （e.g. Copilot）构造 program sketch。
-
使用 TDD （Type driven development）精确指定 program specification。
-
使用 TDD（Test driven development）写测试例 program by example。
-
Click a button on your IDE，自动生成程序。
吾"自思"地认为, 我们也应该多独立去想想/怀疑一下, 不要被官方/主流绑架(不是针对吾没接触过的TDD)
或许我们也可以凭着兴趣/好奇心看看数学的发展史是咋来的(例如 矩阵/微积分/极限 这些…), 然后很多为题就迎刃而解/不攻自破了…(扯远了)
不应该是产品经理口述给AI需求，然后就没程序员啥事了么（
二十年前 OOP 盛行，大家都感叹程序员水平不够，玩不了函数式。
程序员能力的提高是需要时间，我更感兴趣的是如何又快又好的完成程序。 有一段时间觉得可视化编程是未来，后来觉得这是扯淡。 现在编程语言的进化很明显是在在语言本身努力，代码、证明、规格融为一体，而不是代码与证明分离，不是代码与规格分离。
F-star, Spark(Ada那个变体)，Dafny，Idris 已经迈出了可贵的一步，虽然不完美，难用、不完备、库少、慢，但我觉得这是基于文本的编程语言在函数式编程后的下一个台阶，再下一个台阶可能是钢铁侠里那种人工智能辅助系统了，类似交互式定理证明，人类和机器合作，再再下一个台阶，就是类似自动定理证明，机器人自主行动😄
看着眼下漫山遍野的虫子，不由的会畅想下未来没有虫子的代码……
测试驱动是形式化证明弱鸡时候的无奈办法。代码覆盖率 100% 并不能说明没 bug，多么绝望的现实。
现在的计算机算力也不行，还是玩不了函数式