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
形式化证明的方法至少到目前为止,没能大规模应用起来,只能说是核心逻辑,证明一下
coq 可以 extract -> haskell 的
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.
你们老板这么好...
Vim 这是打算彻底干掉 Emacs 了么
那你还不快去学 Perl...
- Do programmers have quiet working conditions?
反正我自己写 JavaScript 的时候,不会去改this
的,我都是用self
的,最讨厌那些改this
的库了...所以后来我就用 Python 去了...
#3 楼 @yedingding 还没到大规模打广告的时候,因为最近掉进别的坑里了...
不给力啊...