常备文档，不要头铁死记硬背。

ok，婊 js 魔怔了，262→334 ……

@ps1aniuge
你似乎不知道啥叫“规范”。
POSIX shell 是屑，bash 有 private extensions，不妨碍 POSIX 标准化了带有 I/O redirection 的 shell command language。
相比之下，ps1 的设计好上那么一丢丢，也改不掉 M$的写 spec 落后的现状。ECMA-262 还落后 VC#几年呢……你指望 ps1 能规范就猴年马月了。
另外，所谓屏幕输出也是你自以为是的笑话，尽管偶然符合事实。tee 命令操作的是标准输入和标准输出。在 UNIX 的万物皆文件的邪教下，对应文件还真没错。下面那个叫你 RTFM 的咣的还真是时候。
另外你漏了 POSIX.1 标准化的 tee 命令还有一个破事：禁止忽略错误。

@svenFeng 0.因为这站还动不动什么验证手机号风评在外，直接写完懒得精简了（否则也不会有那么低级的 typo ）。

1.评估是软件工程(SE)的难题，说白了是 PL 圈外部的事情，PL 圈的立场无视这个倒正常。以 paper 为目的的 PL 圈确实不够格。LZ 不算这个圈子，无所谓 PL 圈规矩，不过至少仍然受到 SE 不可抗力的制约，所以需要惦记。
关于 FV 基本同你的意见。显然 LZ 的东西不算适合 FV 的了。

2.CompCert 当然很有意义，不过对做软件的多数人来说，影响主要就是更了解类似 C 这样的语言和实现方式有多么恶心无能，而不是对具体项目能用得上——特别考虑到有需求不得不用 C 的，往往还会用到 CompCert 不支持的特性。
C 的一些困难实际上是原则性和系统性的。类似之前提过的依赖问题，实际上 C 程序内部就很明显：当运行时调用了一个看不见定义的函数，一旦其中不能排除 UB，一样凉凉。
当然，严格来讲这不是 C 的问题，因为看不清的定义完全可以是其它语言写的，而需要允许这种写法一定程度上是不可抗力。
这种片面要求链接兼容性是工程语言和 SE 的传统问题，不能也不该指望 FV 解决。但是，如果 FV 工具受到限制的现状能推进重视这类工程问题，即便不 FV，也算间接起到了正面的作用。

3.因为强调“通用”，用户就非常不特定了，即便不需要提供同等支持。较真的话，作为最终用户的非专业开发者写配置文件应该也能用得上这样的语言。（ LZ 的设计没法做到达到这个目的的程度另说。）
另一方面，专业的开发者要是缺乏相关背景，对 formal method 的理解普遍是片面的，能理解 BNF 的大部分都不怎么能想象到如何 formalize semantic rules，更别提使用了。
这个我认为也没法指望靠 PL 业界拉动，CS 基础教育说到底是另一个距离差得太远的行业。（至少比物理学拉动数学困难。）
然后，业界的编码水准恐怕很成问题。
这至少带来两个推广问题：
a)不和非 PL 出身的职业用户共享工作习惯，准确理解 /想象用户需求困难，不混 paper 就找不到符合实际的方向，或者脑补容易做的需求过日子，于是越来越容易脱离工业界。
b)当 formal spec 越来越像样——接近被 FV 的代码，flavor 被传到到 spec 上，SE 的各种客观混账限制生效，维护成本和扩展的机会成本越来越没法忍受，更没机会推广给用户，自然内卷小圈子玩了。

4.有充足理由负担成本敢上 model checking 这样手法的个别项目，使用 formal method 和不使用相比，往往是有容易理解的意义的。
但是非特定项目的整体来讲，就很捉急了。

5.关键不是做不到可扩展，而是去扩展时需要靠人完成的工作量。
……以及机会成本和沉没成本。
一旦加上“通用”的需求，这类问题会很容易到处都是。
靠设计个别可扩展 feature 来解决是不现实的，搞不好费了多项式时间去设计实现组合 features，还解决不了线性规模的普遍问题。

其它……我提过比 type 更严重的问题是 phasing。所有你提到的这些语言都逃不出 static 这个圈圈。
加上通用目的的魔咒，static languages 可能是整个没有未来的。搞 formal methods 和 type system 的大部分人大概都还没 smoothness 这类关于抽象能力的概念（明明一定程度上这个是更欠 formalize 的……）。

5.可以。
（就我要的东西，大不了做个到 Chez 甚至 Racket 的 transpiler，不是 CPU 密集基本不会比 native 烂哪去……）

LLVM 的主要问题是你别想省事地在上面实现和 C/C++差太多的语言。也没什么能方便部署的公共运行时，JIT 也很叒鸡的样子。
JVM 的一个问题是……残……比如 Clojure 被迫 X 了 TCO。另一个问题是 bytecode 设计还是挺感人的，实用慎重（ Dalvik 表示情绪稳定）。好的地方是现在有 Graal，别的地方没类似的备胎好用，但考虑要求糊感人的 Java ……还是忘了吧。
CLR 中规中矩一点，不过也不指望比 JVM 好哪去（有的部件性能也不咋地）。
魔改个 lua 什么的还可能有点实用性。习作的话，你要有信心你的语言足够像 C/C++，那用 LLVM 无妨。否则注意了解功能限制，剩下的就是哪个看着顺眼用哪个。
我是没排除 C/C++烂的东西以后还能有这个信心，所以就不折腾了。以后有空了移植个 nanopass 类似物。
但是后端坑太大了，我不觉得要验证语言的设计需要做到这个地步。

3.4 ……其实我建议还是先写（ AST ）解释器。
架空 bytecode 摊子太大效果好不到哪去，而当前实用 native 编译器不得不依赖太多跟后端 py 的特性，太糟心了，而且要通用根本就不是几人年能做到让一般人满意的。
（仅从这个意义上，我就不看好单枪匹马头铁直接设计出来的所谓“编译型”语言。等整出能用的早凉了。）

2.一般意义上就是闭包。用 GC 偷懒回避 funarg problem，或者用 C++这种允许 UB 而不依赖 GC 的设计。
Pascal 的解是半吊子，回避了 upwards funarg problem 却也无法支持 first-class function，不推荐。

@Qiaogui 1.没什么好偷懒的地方，自由存储区（比如操作系统提供的堆）上分配逻辑上 LIFO 的活动记录帧来当作传统的栈。SML/NJ 就是这样做的。
好处是其实不止能实现能避免 stack overflow UB 的栈，first-class continuation 和 PTC 都会省事。
坏处是被当前流行给 ALGOL 开洞的体系结构歧视，即便不考虑碎片问题，不同时实现 GC 就会有 overhead （不过老实说，故意回避 GC 对实现水平要求远远更高）。某些 ISA 上可能还会有标准 calling convention 兼容性的问题。

草，typo，把当前正撸的代码的标识符混进来了…… subsequent→sequent。。。

@svenFeng 我想我基本明白你的意思。不过，LZ 的名义目的一直是“通用”编程语言——所以这里有些微妙的差异——特别是考虑工程可行性的时候。
1.考虑整体工作量上的复杂度，无法指望“容易实现”。
我说的实现，当然，首先是语言自身的实现。所以你说的写（正确的） type checker 更容易这样的局部的着眼点是合理的。
但这和不使用 formal spec 的传统做法相比，这其实也只是在 QA 提升了一小部分（即便相比传统方法的提升是决定性的）；而作为代价，还明显地多出来了一部分：写验证代码。
据我所知，Coq/Isabelle 作为语言虽然有越来越往通用的方向上走的姿势，仍然还是 proof assistant 为中心，不适合直接实现 QA 以外的部分。
（题外话，其实就是 ML 系的语言都有很浓的 DSL 的味道—— pure functional 在某种意义上是注定无法“通用”到哪去的——就像汇编一样。）
所以，维护这样的语言及实现，得至少找到会同时使用非验证语言（实现语言）和验证语言的部分。
除了 IC 验证等极少数领域，这在工程上整体工作量很可能更多，几乎没有换来周知的正面效果。
2.Formal spec 的一个显著作用和预期目的是使 spec 的精确性更容易保持，尽量减小实现的偏差，而提升整个实现环境的质量。
但很遗憾，这个目的除了极端封闭的个别关键嵌入式产品（……比如月球车）外，因为依赖外部系统的关系，基本没法系统性地实现。
因为 formal spec 使用的 formal semantic methods 到目前为止能做到的最符合这个目的的做法，说白了也只是从一个 abstract model 翻译到另一个而已。
假设 formal spec 作为 source model 的描述是无 bug 的，也不能保证实现无 bug。
所以如果 target model 的实现本身不靠谱，翻译之前的 model 再保证没 bug 也挽救不了整个系统的实现质量（只能排 bug 时更容易踢皮球而已）。
举个例子，你如果用 C++当实现语言，整个系统的实现就别指望严格地靠谱了，因为 C++的 normative spec 不是 formal 的，更没有 C++实现宣称 formally verified。
使用公开的资源，你可能只能选择 C99 的一个子集然后使用 CompCert 来实现才能基本达到这种保守的目的——如果有 bug，bug 基本就是宿主环境和处理器厂商的。
然而考虑到 C 对 strict conforming program 的限制，这对实现整个的语言这种任务来讲，基本没啥意义。
3.上面还是理想情况。更直接的实际困难是，你没法指望保证写对 formal spec ……使之符合 informal 的 endorse 用的吹给用户听的设计的意图（至少对设计一个通用语言讲这是必要的，因为你没法指望它的用户具有足够 formal 脑细胞能自动领会你的设计多提供了传统设计没保证的啥）。
因为得分析确认需求，在你造得出替你思考的强 AI 前，这只能是手动的。我不觉得有谁有能力在“造一个通用语言”的目标上满足这里的人员资源。
此外，“有疑问看 proof ”也只是少数维护者才能做得到的事情。在教用户理解如何使用时，还多出来一遍切换 normative formal 和 informal spec 的工作量，这也是人肉的，也可能出错。
如果这个 formal spec 要 publish，我好像也没看到有谁能直接印 Coq 代码上去就算数了……
其实我觉得如果能印 Coq 代码上去大概还是进步的。我不清楚确切理由（也许是灌水的惯性问题），但是现状是，这方面业界人士似乎都喜欢在明显不适合的地方继续滥用 subsequent calculus 之类的东西。
当然，informal spec 这里也不省心。但是讽刺的是，因为后者不要求那么 formal 到必须通过 verfication，反而是更能“容错”的——不少 spec 的 bug 甚至可以延后解决，而不影响实现的进度。
4.非工程的意义上，如果你想写得整体上让人能看得懂，这样做还有摆脱不了 meta language 不够 formal 的问题——以至于不得不妥协，很难整个 formal 到底。
具体来讲，上面的依赖外部系统换成 spec 本身——项目会有外部 spec 依赖。
比如你能拿 Coq 代码当 formal spec，那么你如何判断 Coq 代码作为工具来说是保证能正确表达你的意思的？是不是还要引用 Coq 的 reference ？或者更极端点，直接把用到的部分包含进来？
然而上面说了，Coq 本身仍然相当地 DSL。在通用语言的 spec 里包含 DSL 的 spec，即便这部分只作为 meta language，我觉得仍然是十足的迷惑行为。
（虽然 Robin Milner 等看起来不那么想，实际上还把 ML 剁成一坨坨分开讲，似乎还很能彰显 ML=metalanguage 的样子——但是他们自己在 spec 用的 denotational 的东西和英语显然很不够 ML ……）
5.暂时忘掉上面所有的麻烦，还有个扩展的问题：spec 如何被用户复用以得到一个派生的语言？
如果 spec 的形式是 proof 堆出来的，那么要么这个派生的语言是 spec 规定的严格的保守扩展，要么就得几乎一个个重新（人肉）检视所有 proof 是否仍然能够符合新的需要。
一类具体的实例是本体论扩展问题。通常意义的 formal spec 中，基本只能使用 closed world assumption （除非你开洞允许用户覆盖 type system 相关的 rule，但都这样了，写死在 spec 里还有啥意义……），而真正意义上的通用语言要求 open world assumption。
你如何设计你的 type 以允许扩展加入新的 disjointed type universe 且确保原有的 typing/typechecking rule 仍能 consistent 且有意义？
当然，可以限制被扩展的语言只能作为 meta language 来彻底回避这个问题，但这又让通用打折扣了。

外包？

@svenFeng 不说不重要，但是确定这点重要性本身是重要的吗？有 formal spec 的 spec 能保证在 spec 的意义上就一定质量更高呢，一定更容易实现呢，一定更不容易被误解呢，一定更直接解决当前问题呢，还是一定更容易扩展呢？
退一步讲，就算已知有必要，你用什么方式来确保 spec 内对元语言的正确使用？
这些问题实际上就是 formal spec 为什么通常不是 normative spec 的原因。

当前结论：
1 胖= ¥ 1,514,092 （划掉）¥ 1,473,816

居然还需要出门？（狗头）

@WaJueJiPrince 语文水平是有国界的么。
你能不能讲清楚一点“ Apache 基金会”与“ GitHub ”算是什么鸟技术？
@kevinhwang “不愿意维护老项目，想写新项目”、爱“才能秀出个人的肌肉”或者 go 本身与精英有什么逻辑联系？

@no1xsyzy
在整个 CHM 都是微软已经明确表示过气而不被支持的技术的情况下，我不认为有必要做那么琐碎的推测。用户也未必乐意看到这样。
而且 pdf 阅读器这方面和 chm 体验上是可以类似的。（虽然我的 pdf 直接关联浏览器了。）

关于许可，多提一点：程序和文档分开许可，免得细节破事多。

“无关”的说法不现实。利益相关的观点是被自身立场影响的，而品行如何说到底就是私人道德立场上的观点，从来就不会无缘无故地自动上升为公德。
更符合常理的提法是：诉诸人身这种逻辑谬误暴露观点的不可靠。
对长期输出不可靠观点的，我不觉得有必要多浪费时间。
只要不用来评价具体观点，挖历史可以是评价可信程度的合理优化。并且，挖历史跟把挖出来的历史拿过来用是两回事。

9102 年了还 chm，给个 pdf 又不会要命……