TE
科技回声
首页24小时热榜最新最佳问答展示工作
GitHubTwitter
首页

科技回声

基于 Next.js 构建的科技新闻平台,提供全球科技新闻和讨论内容。

GitHubTwitter

首页

首页最新最佳问答展示工作

资源链接

HackerNews API原版 HackerNewsNext.js

© 2025 科技回声. 版权所有。

FSCQ: A formally verified crash-proof filesystem [pdf]

39 点作者 anishathalye超过 9 年前

3 条评论

anishathalye超过 9 年前
FSCQ is a certified filesystem written and proven correct in Coq. It&#x27;s the first filesystem with a machine-checkable proof that it&#x27;s implementation meets its specification and whose specification includes crashes.<p>The full source code of FSCQ is available online: <a href="https:&#x2F;&#x2F;github.com&#x2F;mit-pdos&#x2F;fscq-impl" rel="nofollow">https:&#x2F;&#x2F;github.com&#x2F;mit-pdos&#x2F;fscq-impl</a>
评论 #10606666 未加载
Natsu超过 9 年前
I can&#x27;t help but think of a couple things:<p>&quot;Beware of bugs in the above code; I have only proved it correct, not tried it.&quot; -Donald Knuth<p>And this bug: <a href="http:&#x2F;&#x2F;googleresearch.blogspot.com&#x2F;2006&#x2F;06&#x2F;extra-extra-read-all-about-it-nearly.html" rel="nofollow">http:&#x2F;&#x2F;googleresearch.blogspot.com&#x2F;2006&#x2F;06&#x2F;extra-extra-read-...</a><p>EDIT: I should have elaborated further. I did not intend to sound like I&#x27;m dismissing this work, because it&#x27;s a cool step forward. It&#x27;s just that this reminded me of those things that happened before.
评论 #10599320 未加载
评论 #10599433 未加载
评论 #10599340 未加载
justinsaccount超过 9 年前
That sounds nice to have, but isn&#x27;t it not as useful without a formally verified crash-proof firmware running on the disk?
评论 #10599297 未加载