C專家編程中對形式化方法的評論現在還是這樣的么？

c專家編程第10章最後，寫了一些對形式驗證的看法。一些摘抄如下：

裘宗燕老師的一篇文章提到了截然不同的觀點: 形式化方法 ｜形式化方法對軟體開發的挑戰：歷史與發展

想諮詢下應該如何看待這個領域。

推薦閱讀裘宗燕老師的那篇文章，

裡面講了近年來基於程序邏輯的互動式驗證的很多重要工作，如CompCert編譯器，FSCQ文件系統，CertiKOS內核。這些項目涉及的相關研究人員像Andrew Appel, Adam Chilpala, Shao Zhong都是本方向的代表性人物。。有興趣的同學可以看看 Deep Specification 項目。國內的話，可能對這方面有所關注的不少人知道中科大馮新宇老師，但是大概兩年前和馮老師聊天時得知其實也有一些其他團隊做得不錯（莫要只看論文。。）。

另外文中還提到了Lustre語言。就我了解的， 有很多基於模型檢查 和抽象解釋做自動驗證相關的工作是針對Lustre語言的，比如kind2-mc/kind2 model checker。順便一說， 國內做模型檢查的人很多。

形式化方法話題甚廣，推薦關注CCF（中國計算機學會）形式化專委。。

Expert C 都是二十多年前的書，Coq 和其它一堆 proof assistant 還處於比較早期的階段，離各種現在看起來自然和趁手的 logic 和工具的出現還有大概十年的時間，作者受限於當時的研究現狀得出那樣的結論也是情理之中的事。相對而言，裘老大的那篇文章立足當下，才是現在對形式化驗證比較中肯的評價。