首页   注册   登录

svenFeng

V2EX 第 181158 号会员,加入于 2016-07-10 19:39:42 +08:00
svenFeng 最近回复了
143 天前
回复了 s1ma 创建的主题 旅行 [多图预警] 北京周边徒步爬山露营组队
群人数超了😨
153 天前
回复了 Qiaogui 创建的主题 程序员 Tripod-语言参考规范(草案)
@FrankHB 看了发现这种 phasing 是合理的啊,理论上除了 evaluation phase,其他 phase 都必须是 static,这是期望行为吧(包括 parsing phase ),也就是这是 feature 啊,理论上任何抽象解释都应该停机,不然就谈不上正确性了,不停机的编译器,那不得 gg。
153 天前
回复了 Qiaogui 创建的主题 程序员 Tripod-语言参考规范(草案)
@FrankHB

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

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

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

对我个人来说,我基本都不会趋向于这么干。。。我更有可能拿 Coq 来写 high-level model and proof,然后再去写对应的 haskell/rust 代码。
153 天前
回复了 Qiaogui 创建的主题 程序员 Tripod-语言参考规范(草案)
@FrankHB 我倒不觉得 static 有啥问题,从代码角度上来说,定理证明作用之一就是顺带提供一个精妙的手段去完成 statically analyse 的工具,要求 total function 也理所当然,从这个角度上来讲,这不是 bug,是 feature😏(逃
154 天前
回复了 Qiaogui 创建的主题 程序员 Tripod-语言参考规范(草案)
@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。
155 天前
回复了 Qiaogui 创建的主题 程序员 Tripod-语言参考规范(草案)
@FrankHB 从我举的 type rules 的来回答,formal spec 可以用 coq/Isabelle 来 formal proof,能保证 sound,不然靠猜想和直觉吗?写 type checker 直接按着 rules 写就好了,就是更容易实现,不会写着写着才发现幺蛾子,每一次扩展都重新加到证明了,更简单肯定说不上,起码更有底气,formal spec 起码比自然语言描述起来准确,最好给个 coq 代码就更完美了,有疑问看 proof 就行了。
155 天前
回复了 Qiaogui 创建的主题 程序员 Tripod-语言参考规范(草案)
@FrankHB 先不管现实语言,你觉得造一个语言之前给一个 formal spec (最好用形式化证明过)不重要?比如 type system 的 type rules 以及证明需不需要?
155 天前
回复了 Qiaogui 创建的主题 程序员 Tripod-语言参考规范(草案)
@FrankHB 🌎你说的我都赞成,但是我感觉我们在跨服聊天😣
155 天前
回复了 Qiaogui 创建的主题 程序员 Tripod-语言参考规范(草案)
@FrankHB 补充一下λx. (+ x x)是将类型写为 forall a. a -> a -> a 的情况编译不过
155 天前
回复了 Qiaogui 创建的主题 程序员 Tripod-语言参考规范(草案)
@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 写着写着就不想写了,浪费时间。
关于   ·   FAQ   ·   API   ·   我们的愿景   ·   广告投放   ·   感谢   ·   实用小工具   ·   2579 人在线   最高记录 5043   ·     Select Language
创意工作者们的社区
World is powered by solitude
VERSION: 3.9.8.3 · 10ms · UTC 14:05 · PVG 22:05 · LAX 06:05 · JFK 09:05
♥ Do have faith in what you're doing.