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