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

http://en.wikipedia.org/wiki/QuickCheck

http://libre.adacore.com/tools/spark-gpl-edition/

https://github.com/openETCS/model-evaluation

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

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

#2 楼 @chenge

http://www.staff.science.uu.nl/~swier004/Talks/BrouwerExtraction.pdf

coq 可以 extract -> haskell 的

#81 楼 @Rei 恰恰相反哦，你现在是在写直接给客户用的东西哦。你可不能leave errors in code for customers to find.。我用各种脚本来胶水才是正常的...

#5 楼 @kgen 效率也可以很高的...难道你没听说过封闭式开发...

#77 楼 @Rei 损失大了，损失大量机会成本...

Static analysis of C code is useful, but if you are thinking of starting a new project, choose a sensible language! Don't start new projects in C or C++, or dynamic languages like Perl and Python which leave errors in code for customers to find.

http://people.redhat.com/~rjones/cil-analysis-of-libvirt/

你们老板这么好...

Vim 这是打算彻底干掉 Emacs 了么

#35 楼 @Rei 非常建议你去看一下 Zed Shaw 是怎么吐槽 GitHub 的

#2 楼 @jasl 用 Perl 有机会早日加入文艺青年的行列啊...

那你还不快去学 Perl...

1. Do programmers have quiet working conditions?

http://www.joelonsoftware.com/articles/fog0000000043.html

反正我自己写 JavaScript 的时候，不会去改this的，我都是用self的，最讨厌那些改this的库了...所以后来我就用 Python 去了...

#3 楼 @yedingding 还没到大规模打广告的时候，因为最近掉进别的坑里了...

不给力啊...

#11 楼 @kevinxu node.js 怎么和 stackless python 比，搞不好连 Emacs 都拼不过的...

#39 楼 @luikore 必须二维码...

#6 楼 @jasl 这意味着你该紧跟 Zed Shaw 的脚步...

http://joearms.github.io/2013/03/28/solving-the-wrong-problem.html

#39 楼 @luikore 那你来写一个能让先有的文档生成工具都能轻松用上的 PostScript 啊...效果不能比 xeCJK 还烂...

#28 楼 @xds2000 所以坑爹啊，我那么看好 OpenShift