V2EX = way to explore
V2EX 是一个关于分享和探索的地方
现在注册
已注册用户请  登录
V2EX  ›  svenFeng  ›  全部回复第 1 页 / 共 8 页
回复总数  141
1  2  3  4  5  6  7  8  
2021-12-29 13:13:20 +08:00
回复了 oblivion 创建的主题 宽带症候群 陪伴了近 10 年的移动号码被封停了
@wonderfulcxm 手机号有个非常大的问题是他会被重利用,也就是过一段时间你发现自己废掉的手机号被别人启用了,这时候你绑定的那些服务就会有安全问题。
2021-04-16 15:51:43 +08:00
回复了 AhogeK 创建的主题 问与答 有用 hhkb 的吗?适应了两天,反而老键盘的 ctrl 有点不习惯了
用 SpaceFn 吧,可以看一下: https://v2ex.com/t/755046#reply1 ,也许能解决你的问题
2021-03-23 23:19:12 +08:00
回复了 svenFeng 创建的主题 求职 求一份海南或是远程的工作
@4kingRAS
@hitfxw 做区块链
2021-03-05 10:48:02 +08:00
回复了 svenFeng 创建的主题 求职 求一份海南或是远程的工作
@haijianyang 我先试试看情况吧
2021-03-03 11:03:06 +08:00
回复了 svenFeng 创建的主题 分享创造 写了一个 Linux 下的键位映射软件,大家有需求可以试试
已经支持指定键盘功能。
2021-03-01 18:33:50 +08:00
回复了 svenFeng 创建的主题 求职 求一份海南或是远程的工作
@wzcloud 有这种预感
2021-03-01 14:39:15 +08:00
回复了 konnga403 创建的主题 海口 从上海回海口快一年了,聊聊感受
@kime2019 有群号吗?
2021-03-01 12:14:28 +08:00
回复了 svenFeng 创建的主题 求职 求一份海南或是远程的工作
@roth 我找找看,多谢
2021-02-27 18:06:57 +08:00
回复了 konnga403 创建的主题 海口 从上海回海口快一年了,聊聊感受
@karnaugh 你建个群吧,再发个帖子 2333
2019-06-22 16:31:54 +08:00
回复了 s1ma 创建的主题 旅行 [多图预警] 北京周边徒步爬山露营组队
群人数超了😨
2019-06-12 14:32:55 +08:00
回复了 Qiaogui 创建的主题 程序员 Tripod-语言参考规范(草案)
@FrankHB 看了发现这种 phasing 是合理的啊,理论上除了 evaluation phase,其他 phase 都必须是 static,这是期望行为吧(包括 parsing phase ),也就是这是 feature 啊,理论上任何抽象解释都应该停机,不然就谈不上正确性了,不停机的编译器,那不得 gg。
2019-06-12 01:37:14 +08:00
回复了 Qiaogui 创建的主题 程序员 Tripod-语言参考规范(草案)
@FrankHB

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

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

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

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