@wonderfulcxm 手机号有个非常大的问题是他会被重利用，也就是过一段时间你发现自己废掉的手机号被别人启用了，这时候你绑定的那些服务就会有安全问题。

用 SpaceFn 吧，可以看一下： https://v2ex.com/t/755046#reply1 ，也许能解决你的问题

@4kingRAS
@hitfxw 做区块链

@haijianyang 我先试试看情况吧

已经支持指定键盘功能。

@wzcloud 有这种预感

@kime2019 有群号吗？

@roth 我找找看，多谢

@karnaugh 你建个群吧，再发个帖子 2333

群人数超了😨

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

@FrankHB

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

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

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

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

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

@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。

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

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

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

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