Ruby China

Ruby 正确性证明的问题

chenge · 2013年05月11日 · 最后由 bhuztez 回复于 2013年08月02日 · 2380 次阅读

目前主要还是靠测试来辅助，测试本身辛苦而且不可靠。

正确性的证明目前的进展如何？有多大程度的在实际应用？

haskell 这样的语言可以改善静态分析和正确性证明。

提个话题，看有兴趣否？

1 个赞
bhuztez #1 2013年05月11日

coq 可以 extract -> haskell 的

chenge #2 2013年05月11日

#1 楼 @bhuztez coq 可以辅助证明 haskell，是这个意思么？

bhuztez #4 2013年05月11日

All attempts to use formal methods to derive software from requirement specifications break down as soon as we try to use them on realistically large and non-deterministic systems.

The same is true of attempts to formally prove the correctness of programs.

The most commonly used paradigm for SW development is “trial and error”.

http://www.erlang-factory.com/conference/London2011/speakers/MikeWilliams

形式化证明的方法至少到目前为止，没能大规模应用起来，只能说是核心逻辑，证明一下

chenge #6 2013年05月11日

网上说 coq 用于法国的地铁软件，无人驾驶，效果很好。还是很鼓舞的。 用于 os 这样的似乎还不现实。

bhuztez #7 2013年05月11日

#6 楼 @chenge 终极问题是你怎么知道 spec 是符合真实需求的。哪怕你证明了你的实现完全符合 spec。spec 不符合需求也是白搭。

bhuztez #8 2013年08月02日

#6 楼 @chenge 想起来，好像 seL4 的内核被形式化证明过

需要 登录 后方可回复, 如果你还没有账号请 注册新账号