Tripod-语言参考规范（草案）

这么长，有热心群众画一下重点吗

精神可嘉，加油👍

不错，楼主居然真的动手做了点东西，聊胜于无。

粗粗读了前几章，感觉就是在 C 的基础上稍微修修补补？

虽然我知道我的问题可能有些 naive，不过我还是要问一句为什么要有 /** */ 的注释。

像是基于 Object Pascal(Delphi) 改编的，糅合了一点 C。但没看到什么特别新的东西

我觉得我无法忍受在 readme 啥都不写然后 repo 里放 pdf 文档这种蠢事。

PDF 排版很优秀啊。

希望可以增加一些小 example，与别的语言对比，体现你这种语言的优点，这样会直观很多。

唉，我觉得吧，咱能不能多读点书、paper 再出来搞个大新闻，你这除了对 C++拙劣的模仿还有啥？ PL 有些东西已经很成熟了，不好好学习瞎整除了误导别人还有什么意义？

sum type 这么自然的结构没有，还 null ？噢，还引入了 nil。。。

template 作为 meta language 虽然可以做泛型来用，但是我很好奇怎么保证 parametric polymorphism 的 forall 语义，不保证的话像 C++一编译一路 SFINAE 就狂吐错误么？再说了，你这也没有 concepts 做限制吧。

你号称解决 C++的遗留问题，你知道你不但没解决这些问题，还更垃圾了么？

你写的这么多，还不如给个 Semantic Specification，不用说，连 spec 都没有，你估计都没想过证明你的 type system 的正确？写编译靠蒙吗？

lz 加油

建议你多看看这近 10 年，新诞生的语言到底优化和解决了啥。

你这说实在的不如 cpp，特别是 17 以后的特性

你还没有上大学吗，如果是中学生，这 pdf 还能理解。大学的话，建议你练习一下论文怎么写的，这样下去你怕是毕业论文都够呛
先把现有的语言学好吧，看你这写的，现有的语言都没搞明白
https://i.loli.net/2019/06/08/5cfb53f11181780894.png

@trait 摆出一副世外高人的样子, 那你说说你截的图里正确意思呗.

@trait 看了你的所有回复帖子, 都是一副欠揍的语气

@Aumujun 又是个连基本的 pl 知识都不懂的上来送人头了 搞清楚什么叫 scope http://lucacardelli.name/papers/typesystems.pdf http://faculty.cse.tamu.edu/hlee/csce314/lec09-scope-type.pdf
你也就只会再网上无能狂怒，我等着你揍

@Aumujun 连个 scope 这种语言基本知识都能让你产生世外高人的感觉，你菜的太真实 block

楼主加油，继续改进

初略看了一下基本语句，为什么关键字不统一大小写呐，Else 这编程很烦啊, 另外 do 语句(??)和不加 do 有区别吗！！？

关注后续

看了一下，怕是连我们大一编译原理课程布置的 toy language 还要不靠谱。回去看看龙虎书吧

@qgs 以 js 为例，是有返回值的 https://github.com/tc39/proposal-do-expressions/blob/master/README.md 楼主这个设计我不做评价
但是这个是 Expression

有 bnf 吗？

如何评价语言这种事情，怎么少得了🌍
手动召唤 @frankhb

@inhzus 有的在末尾，建议看完再喷
槽点太多不知道要喷什么了


我前老板说得好，不看苦劳，只看结果。
楼主做了一些工作是好的，但是没有价值，是苦劳。

加油！

@svenFeng LZ 的煋闻早就贴了。（看了大概就不会要啥 spec 了……不过题外话，我倒是强烈支持你这话拎过去跟 Rust 党说去。）
PL 的东西成熟和 LZ 的不成熟倒是没什么直接关系。LZ 这方面出的问题首先是他没找对什么“遗留问题”，而不是解决上出了问题。（但是我寻思你也同样没指出这些问题……）
另一方面，当代主流 PL 业界扯乎的幼稚设计整个也没好哪去，比如言必称 type，连 type 满足什么需求八成都没搞清楚。
在这个前提之下，sum type 算什么“自然的结构”？多糊上个 natrual transformation 是不是更自然了？
啥叫 forall 语义？跟 SFINAE 有啥关系？

@WispZhan 哪壶不开提哪壶…… C++17 以后的大多数东西，都是需求方面有大量的表面共识但设计起来各说各话，做出来的特性怕是快人人喊打了。

@trait 2young。你一开始的截图里是如果按现有的语言习用的术语理解，是有很明显的有低级错误的：LZ 看起来连声明和定义的区别都没搞清楚。但撇开这种设计的实例（至少有 C 和 C++）本身的流行程度，“定义”其实是非常 specific 的设计，和一般的 PL 理论并没什么关系。（ C++要定义很大程度上是为了 ODR，你能把 ODR 糊到哪家 PL 理论上去？）如果能在 spec 中另外给出“定义”之类术语的定义，也是可以说得通的，这同样和一般的 PL 并没什么关系。
可能你会觉得违反“ PL 常识”是岂有此理，但是现有工业语言还就是这样做的。例如，ISO/IEC 14882 事实上钦定 polymorphic 的外延就是指某些特定的 inclusion polymorphism，全然不顾 parameteric polymorphism 云云。还有，大坨的语言 spec 根本就没分清楚 variable 和 mutable object，但非得这样说在 spec 本身的 scope 里也说得通。
所以你引用的文献就比较匪夷所思了。更麻烦的是，还有相当严重的质量问题。跑题先不论（第一篇和啥叫 scope 有关么……），至少这坨 ppt 里的东西并不比 LZ 给的内容更严谨。
作为例子，这里首先根本就没说清楚什么叫 variable。即便是笼统地概括，也跟正式的(normative)东西差的老远。按实际影响比较广的定义（参考 ISO/IEC 2382 ），variable 是一个一大箩筐东西的四元组，其中并没有什么 type。另外，lifetime 套在 variable 上是说不大通的。为了讲 type （ checker ？）而夹带不够全面的私货，这在教学的意义上也是可耻的。（就不说氵到啥叫 typing 都没敢说了。）

@FrankHB 我截图是作用域你跟我扯一堆什么定义声明 var lifetime，来，你跟我说说，楼主作用域给的定义什么叫做“可见”，谁可见？？？

@FrankHB forall 就是全程量词∀，forall 语义就是全程量词的语义啊，C++ template 本质是类型宏，要刷出类型再类型检查，根本不能保证 forall 语义，比如λx. (+ x x)在 rust、haskell 之类的是编译不过的，而 C++则没问题。

Sum type 很自然啊，sum/product 这两种组合数据的代数结构本来就是自然而然的啊，用 product 虽然可以表达 sum type 的逻辑，但是用起来十分费劲（比如你看看 golang ），你说的是 natural transformation 吧？ damn，不学猫论跟你们吹逼就是吃亏。

C++的遗留问题太多了，非得一个个列么。。。我回 LZ 写着写着就不想写了，浪费时间。

@FrankHB 补充一下λx. (+ x x)是将类型写为 forall a. a -> a -> a 的情况编译不过

@trait 怎么话都说不利索……

1. 你看清你截的图了？

a)“什么定义声明”就是截图里提到的内容。

b) 第一句就指出“标识符在程序文本中可见”，哪来的“谁可见”的问题？

c) 可见性(visibility) 和所谓定义之类的术语在 ALGOL-like 的工业界 spec 里还是挺流行的。这跟“什么定义声明”说白了是一个档次的常识。你如果不是习惯性看漏和装着不知道，那说明你欠缺这方面的知识基础。

2.你看清我的回复了？

什么 var lifetime 婊的是你引用文献的质量明摆着不合格。

是不是要我更明白地指出你引用文献的水准更不合格呢？

@svenFeng 你觉得拿 natural transformation 开刷我会不清楚全称量词是啥么……

（真的，我当时已经输入了“就现在这种 PL 还有资格管一个设计里有没有 universal quantification 么”，想了下嘲讽性质太强就删了。）

你的关于 forall 的说法，按我现在的理解重新表述一下：

要 implicit typing/structrual type inference，要 first-class higher-order type，要 sound 能 typecheck。

然而我的意思是：

1.不，真的不都需要 nominal typing，即使是为了 typecheck。

2.就算非要这样……都这样了，为啥不直接更具体点，比如上 System F 呢。
（ Undecidable xxxxx ……嘛，只要没洁癖非得干掉 type annotation，这实际上真的不是啥大事儿。）

“ sum/product 这两种组合数据的代数结构本来就是自然而然”这个……还行吧。
但是之前讨论的默认上下文显然是指塞到语言的内建特性里。把这两者混为一谈就很不地道了。

要我说的话，继续上面的思路：
……
哦，还得解决 metaprogramming 破事多的问题是吧。
……
（跳得有点远……）
……
嗯？我为啥需要内置 type system 呢？

当然，这跟 LZ 的设计无关。

C++ 的遗留问题罄竹难书算是普遍共识了，这个也没啥问题。像 C++ 把 class template 排除出 type 这点我深恶痛绝，不过这不是 template 本质是什么的问题。后者的问题(phasing) 比类型系统的问题更严重。

@FrankHB 🌎你说的我都赞成，但是我感觉我们在跨服聊天😣

@svenFeng LZ 也在和你们跨服聊天啊。。。。（虽然这楼里我压根还没理过。）
不开玩笑，LZ 虽然眼界不咋地口味奇特，但是已经上手的部分比这里大多数人清楚多了。虽然没自己做过的会有这种印象也不奇怪。
另一方面，眼界问题也被这个拉平了一部分。比如 LZ 经过提醒起码知道要有像模像样的 spec 了，而你张口就来要有 semantic specification，好像 LZ 提供的东西压根就不包括这些内容一样……于是，看起来是指 formal spec 了？那么，你真的清楚现实有多少语言的这部分 spec 是 formal 的么？

@FrankHB 先不管现实语言，你觉得造一个语言之前给一个 formal spec （最好用形式化证明过）不重要？比如 type system 的 type rules 以及证明需不需要？

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

@FrankHB 从我举的 type rules 的来回答，formal spec 可以用 coq/Isabelle 来 formal proof，能保证 sound，不然靠猜想和直觉吗？写 type checker 直接按着 rules 写就好了，就是更容易实现，不会写着写着才发现幺蛾子，每一次扩展都重新加到证明了，更简单肯定说不上，起码更有底气，formal spec 起码比自然语言描述起来准确，最好给个 coq 代码就更完美了，有疑问看 proof 就行了。

@FrankHB 大大，感谢您一直以来的支持。
我发现靠别人进行实质性的帮忙还是靠不住，我还是决定自己先动手写个编译器，有以下几个问题想咨询一下大大：
1. 对于各种形式的递归，如果编译器要将它们实现成为可以无限递归的形式（不受栈的限制），该怎么做？
2. 对于 Pascal 那种形式，可以进行内部定义以及重重嵌套定义该如何实现？
3. 该使用 LLVM、JVM CLASS、或者其它低级语言作为底层实现？
4. 如果使用 LLVM，哪些点应该重点学习？哪些可以一笔带过？因为 LLVM 的资料太大，很繁琐，而且向后兼容性也不好，FreePascal 都不推荐使用 LLVM 的编译器。
5. 可不可以翻译成其他的高级语言，类似于 C/C++，直接的 JAVA 源代码等？。

@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 来彻底回避这个问题，但这又让通用打折扣了。

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

有些人戾气太重了,你给不出或者不想给实质性的帮助，就请闭上你的臭嘴

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

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

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

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

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

@FrankHB 谢谢

@FrankHB 你写的好多- -'''

1. 工程上的工作量的问题，说实话就是成本的（时间、金钱、人等）问题，有没有效果这点是很难讨论的，因为工程上大家很少评估你一个程序 bug 少，往往评估的是性能、feature 等等，总而言之，质量这件事情在工程上真的很不好量化，所以真正用 FV(formal verification)的地方都来自于学院派或有一定底气的公司。

用 FV 从领域上来讲，更容易区分，用 FV 的都是质量和成本真正可以讨论的领域，比如部分硬件和嵌入式系统，这些系统一出现 bug 的后果就是灾难的，所以在这些领域 FV 会比其他地方常见，还有分布式和并发系统，这是因为时序太复杂了，普通的测试一般搞不定，所以有时候也可以看到 FV 的影子，比如 Lamport 的 TLA+（ lamport 的很多 paper 都会有相应 TLA+代码，遇到不理解的问题，直接看代码简直太舒服了）

2. CompCert 这个工程我觉得还是有意义的，整个系统用上 FV 真是很少，但是有些库比如一些高并发、分布式核心逻辑（一致性协议、多阶段提交等）等等用 C 写完后，编译给 Coq 做证明是非常有意义的，不然真是很难写对。。。

3. 用户这件事情，我觉得看做什么，普通的用户当然不行，但是对于开发者，把 formal spec 已良好的方式展示给用户这点太重要了，比如你要写某语言的静态分析，严格的 BNF 和 Type Rules 等等真的太重要了，写各种系统写扩展（比如写 Mysql 分布式中间件）没有 Formal spec，简直了。。。我觉得这就是业界应该改进的地方。

4. 我觉得整个系统用 FV 这种场景用 Coq 这样来做定理证明还是很难的，但是 Model Checking 是有意义的，一方面 check 整个系统的逻辑，一方面可以把 formal spec 当文档，比各种瞎糊的人肉文档靠谱太多了。

5. 可以扩展和派生这点，也不难吧，Coq 这样的定理证明器，直接看 Theorem(Type)就很清晰了，扩展就是直接加新的 Theorem 就好了。Model Checking 如 TLA+基于集合论虽然口味奇特，但是也是有可扩展 module。Spec 一般都是期望行为，具体的只要可以能被证明是符合需求的，那就没问题，随便改。

其他，关于 FV 方向性的探索方向一直都有，比如 Coq 本身不是通用语言也可以作为 Source 直接编译到通用语言啊，比如把 Coq 代码编译到 Haskell/Rust/ML，这都是可以的尝试，在比如 Idris 本身就是通用语言，因为支持 DT(dependent type)也可以做定理证明，抛开这些 refinement type 这些年也挺不错的吧，不用堆 proof，还有 Model checking 就更简单了，堆机器跑就好了，也不用费心思写 proof。

@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 的……）。

@FrankHB 我倒不觉得 static 有啥问题，从代码角度上来说，定理证明作用之一就是顺带提供一个精妙的手段去完成 statically analyse 的工具，要求 total function 也理所当然，从这个角度上来讲，这不是 bug，是 feature😏（逃

@svenFeng 当要把一长坨 spec 当代码来维护的时候，就会容易发现一些尴尬的问题，比如缺少 ad-hoc 的特例规则就没法 late binding，需要单独的 reflection 并且要有很多幺蛾子才能实现对，static 和不 static 的类似废话不得不重复，pattern sublanguage 之类的马甲越来越多并且设计上难以去重……所有这类关于可修改性的问题根本都来源于不切实际的 static phasing 的设计。这根本上就是需求理解偏差：通用意义上真正需要的只是保证有限的局部依赖来确定语言的解释的局部有序关系——例如根据某一类特定的计算决定另一类的求值结果，而不是非得具体到预设一坨全局特性集合然后映射到不相交集合甚至干脆直接分层映射到一坨序数上去。后者本质上是一种对实现细节的抽象泄露，一定程度违反了最小特权原则。

@svenFeng 换句话说，没很具体的问题域，一般本来就根本不应该存在全局意义上的 static 不 static，非得预设 static 和不 static 两类性质已经一定程度放弃了能做的不少必要的事情了，有这种 feature 就通用不到哪去。

@svenFeng 关于定理证明你说得没错，因为定理证明本来就是一个相当 specific 的 domain。
问题在于，从 DSL 里 extract 出 general-purpose language 的做法，比反过来用 general-purpose language 去 derive 不同 DSL 的做法凭空多出不可忽视的工作量，却没有多少现实收益。
后者的做法先不算 derive （因为习惯上只有反过来接着 extract ），在这个 domain 里也就 ML 勉强能算。但是 ML 的问题嘛上面说过了，再加自身扩展起来也很疼，改 spec 不容易，加新 feature 照样得考虑大坨具体 feature 之间的关系，跟真实的 general-purpose 差远了……

@FrankHB

我没明白什么是 phasing - -'''

这两种双向转换说不上哪个好那个差吧，比如从把 C 编译到中间语言，然后 Coq 写证明，就是写 C 舒服，用写证明蛋疼。

而把 Coq 代码 extract 出 haskell 代码是写证明简单，extract 出来的代码质量可能不可控，写 Coq 代码也是件不怎么爽的事情。

对我个人来说，我基本都不会趋向于这么干。。。我更有可能拿 Coq 来写 high-level model and proof，然后再去写对应的 haskell/rust 代码。

> 我没明白什么是 phasing - -'''

cf. The Definition of Standard ML
Chapter 1, para. 3, 4.

> 这两种双向转换说不上哪个好那个差吧

这显然有问题的。首先转换相比之下是凭空多出来的步骤，如果是兼容历史遗留问题还能理解，对新的项目有什么积极意义？
然后更严重的问题是 spec 本身。
你提的语言里要么默认了，要么明确指出这种和我要求的相反的做法，如 SML 这种为了 formal spec 偷懒，撑死只允许实现混淆 static 和 dynamic phase，而 spec 里是写死了的。但这种 formal spec 的东西其实是没法直接用于不区分 phase 的实现的，实际上变相歧视了更自由的实现（类似 C/C++都明确回避要求编译，但不 AOT 编译实现起来就是吃亏）。
同时，这样 formal spec 更复杂了，而不是标榜的简单了——所谓的简单，是作者自认为的写起来的简单而不是统计写出来东西有多少能客观度量的复杂度的意义上的简单，本质上就是无视元语言的复杂度的鸵鸟政策罢了，就像 AOT 编译把调用编译器的 penalty 无视以后自以为比 JIT 高效一样（ AOT 性能的问题还就是 phasing 破事的另一个具体例子）。
你感觉不出这个问题，可能是因为你和大多数用户一样只使用到现有资源的某一小个子集。比如你用 C，不理解 LLVM 和 cfe 的实现以及 ISO C 的 rules 有多蛋疼，也不是不能干活。但对想要把 spec 垂直地复用到实现上游和下游各个层次、去除其中的重复冗余的 hacker 来说，这是显然不够的。
现在的业界被动适应的这个问题并不光彩，大体思路就是算力不够堆机器，人力不够 996。这是不可持续发展的，同时分工过头导致几乎禁绝垂直复用。虽然能多搞点就业多吹 GDP 吧……

@FrankHB 看了发现这种 phasing 是合理的啊，理论上除了 evaluation phase，其他 phase 都必须是 static，这是期望行为吧（包括 parsing phase ），也就是这是 feature 啊，理论上任何抽象解释都应该停机，不然就谈不上正确性了，不停机的编译器，那不得 gg。

@FrankHB 大大，昨天我看了您的回复，我自己也想了许久。最终还是决定以第 4 种类似的方法实现，因为我发现如果直接翻译成现成的高级语言是有些不现实的，源语言总是会受到目标语言的制约，导致与语言特性相关的不同的底层实现会变得异常困难，所以我考虑再三，还是决定以一个基于寄存器字节码解释器的形式实现（不用栈式是因为用起来不方便），不过我不想依赖于 JVM 和 DVM，以及 LLVM，我打算自己从头开发字节码，关于这方面，想咨询一下您的看法。您对有关设计字节码的书籍有什么好的推荐吗？

@svenFeng 不合理。
1.你忽略了 phase 可以允许让用户指定的设计。保证停机最终是用户的责任。
另外，做编译器基本上不会是实现语言的直接的目的，所以可以反过来想：“能停机的实现的一部分才叫编译器”。停不下来嘛就凉拌。
2.你忽略了 static 之间也不完全是一回事。
（虽然如果不忽略继续头铁 static 的话可能会进另一个坑，比如 static_assert 大战#ifdef。只是这通常没有 std::integral_constant 和 integral type 没法合并的问题这样恶劣罢了。）

@Qiaogui 坑太大，不太值。
因为需要 trial & error 成本太大，我回避从头开始造字节码的设计，对这方面了解不够 。

@Qiaogui 现在进展怎么样了?