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

科技回声

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

GitHubTwitter

首页

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

资源链接

HackerNews API原版 HackerNewsNext.js

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

Writing a Compiler by Proving It Correct

139 点作者 kachnuv_ocasek超过 9 年前

4 条评论

hbbio超过 9 年前
Interesting work. I don&#x27;t remember who said that &quot;formal verification is the way of the future... and it&#x27;s going to stay that way!&quot;<p>Quite strange that the article doesn&#x27;t mention CompCert though, which has an extensive bibliography:<p><a href="http:&#x2F;&#x2F;compcert.inria.fr&#x2F;publi.html" rel="nofollow">http:&#x2F;&#x2F;compcert.inria.fr&#x2F;publi.html</a><p>Edit: The person I quote is a researcher in formal verification, I think it&#x27;s Gérard Huet from Inria.
评论 #10577179 未加载
skybrian超过 9 年前
It looks like this compiler never actually reports any errors. (It uses the Maybe type, so you just get nothing.)<p>I appreciate that it&#x27;s a toy compiler, but I really wish people wouldn&#x27;t leave that out. The quality of a compiler&#x27;s user interface almost entirely depends on its error messages, so it&#x27;s important to demonstrate how that&#x27;s done.
评论 #10579021 未加载
nv-vn超过 9 年前
This got me thinking, how feasible would an implementation of APL be as a DSL embedded inside of Agda (or some other similar language)?
fizixer超过 9 年前
And there&#x27;s not one mention of the word &#x27;optimization&#x27;.