编程语言与软件工程2018arxiv.org
KRust：Rust 的形式化可执行语义
KRust: A Formal Executable Semantics of Rust
专业 · 约 90 分钟读完前置知识：Rust 基础、操作语义、K 框架
导读
这篇论文用 K 框架为 Rust 的一个子集编写了可执行的形式化语义（KRust），也就是一个在形式化系统中可直接运行的 Rust 小解释器，并演示了用它证明程序性质（如 GCD 算法运行时间）。作者自述该语义远未完整，只是通往完整 Rust 形式化的一小步。
HN 关注点：Rust 缺少官方形式化语义，而 HN 读者既关心这类工作的实际覆盖范围与可用性，也关注它与 Rust 官方形式验证工作组、K 框架既有 C 语义之间的关系。
HN 评论精选
这几条评论里：支持 1 质疑 1 补充 1 亲历 1
质疑Rust 社区已有官方形式验证工作组，而这篇论文的子集太小、缺少新结果，借用检查建模也很局促。
在最近的柏林 Rust All-Hands 上，几个独立研究 Rust 语义验证的团队决定成立一个工作组（见 internals.rust-lang.org 的公告）。我不认识这篇论文的作者，说明参与的人可能比我们想的还多；如果读者中有人也在做，欢迎联系工作组。关于本文，我引用 reddit 上的一条评论：「看起来他们用某个形式化系统为 Rust 的一个极小子集写了��释器，但子集非常小，也没得出什么新结果。他们举的证明 GCD 运行时间的例子在几乎任何过程式语言里都成立，只需改改语法。他们实现了一个很简单的借用检查模型，但子集似乎不支持类型签名中的引用，所以连借用检查的跨过程效果都建模不了，只能表达一些纯局部的别名限制。作为在 𝕂 里写 Rust 形式语义的第一步，这还不错，但……」
kibwen查看英文原文
At the recent Rust All-Hands in Berlin a few groups of researchers independently working on verifying Rust's semantics decided to form a working group to focus their efforts (see the official announcement at https://internals.rust-lang.org/t/announcing-the-formal-verification-working-group/7240 ). I don't recognize any of the names on this paper from there, so it looks like there may be even more people working on this than we thought, and if that also happens to encompass anyone reading this comment, feel free to reach out to the working group. :) Regarding the OP, I'll quote a comment from reddit: https://www.reddit.com/r/rust/comments/8g6mam/krust_a_formal_executable_semantics_of_rust/ "It looks like they wrote an interpreter for a small subset of Rust in a particular formal system. But the subset is extremely small, and it doesn't look like they derived any novel results from this. The examples they give, of proving the running time of a GCD algorithm, would work in pretty much any procedural language; it's pretty much just a syntax modification away from the same example in any language. They implement a very simple model of borrow checking, but their subset doesn't seem to support references in type signatures, so it doesn't seem like they can even model any inter-procedural effects of the borrow checker, just some purely local restrictions on aliasing. I suppose that this is a good first step if you want to write a formal semantics of Rust in 𝕂, but it seems like there's not really enough here yet to be of interest."
补充KRust 与 K 框架现有的 C 语义一脉相承，可延伸出 Rust-C 互操作验证等有价值的应用。
这用的底层工具正是支撑 KCC 和 RVMatch 的那套（github.com/kframework/c-semantics、runtimeverification.com/match）。这正是我希望有人去做的事，至少是第一步。第二步是基于已有的 C 语义来做 Rust 语义，这样可以支持很多事：Rust 到 C 的编译器、防御 Karger-Thompson 攻击、乃至验证 Rust 与 C FFI 代码的交互；将来我这边还能用 C 的工具链来验证等价的 Rust 代码。
nickpsecurity查看英文原文
This is the same underlying tool that powers KCC and RVMatch. https://github.com/kframework/c-semantics https://runtimeverification.com/match/ Exactly what I’d hoped someone would do. Well, the first step anyway. The second step was doing a Rust semantics in terms of the C semantics already done. That allows quite a few things like Rust-to-C compilers, defeating Karger-Thompson attack, and potentially verification of interactions of Rust and C FFI code. On my end down the line, also use of C tooling for verification of equivalent Rust code.
支持Rust 的类型安全性使形式化核心语言能贴近真实语言，不像 JS/C 的核心语言要大幅改造。
太棒了。让我兴奋的是，终于有一个正在流行起来的语言（Haskell、OCaml 我觉得还算小众），其用于形式语义的核心语言和它本尊非常接近。像 JavaScript、C 这类语言，形式语义用的核心语言必须去「补」类型系统里的各种不安全漏洞，结果核心语言和它要建模的语言看起来差别很大。
mlazos查看英文原文
This is awesome. It also makes me really excited that finally there's a language that's catching on (I consider Haskell, OCaml and the like to be niche) where the subset of the language that is used for a formal semantics is very similar to the language being modeled. I feel like with Javascript, C and other similar languages the core language that is used in a formal semantics has to "patch up" all of the unsafe holes in their respective type systems, and as a result the core language ends up looking a lot different from the language it is intended to model.
亲历作者承认工作远未完成，呼吁更多人参与推进完整 Rust 形式化。
我是本文作者。这个语义远未完成，我还在继续做。完整形式化 Rust 并不容易，KRust 目前只是非常非常小的一步。现在它可能还「没用」，但我认为只要更多人参与，最终会有一个完整的版本。
iuppiter查看英文原文
I am the author of this paper. The semantics is far from complete and I am still working it. It is not a easy to formalize Rust completely. KRust is now just very very small step towards that. It may be not "useful" currently, but I think there will be a complete one if more people work on this.
相关资源
从这篇论文所有 HN 讨论帖的全部评论里整理出来的链接。
历次讨论
- 2018Hacker News 讨论帖148 分 · 48 评
同领域还值得读
Google 的软件工程（2017）
Software Engineering at Google (2017)
介绍了 Google 的软件工程实践，包括其单一代码库（monorepo）、几乎全部开发在主干进行而非分支、代码审查、构建系统 Blaze、协议缓冲区等工具与流程，并讨论了频繁重…
编程语言与软件工程2017 · 1,127 分 · 465 评 · 引用 15入门 · 约 45 分钟编辑精选Peter Naur：编程作为理论构建 (1985)
Peter Naur – Programming as Theory Building (1985)
Peter Naur 1985 年的经典论文《Programming as Theory Building》提出：编程的本质不是写代码或文档，而是在程序员头脑中构建对程序及其运行…
编程语言与软件工程2016 · 629 分 · 74 评入门 · 约 45 分钟编辑精选SciPy 1.0：Python 科学计算的基础算法
SciPy 1.0: fundamental algorithms for scientific computing in Python
这篇发表于 Nature Methods 的论文介绍了 SciPy 1.0——Python 科学计算生态的基石库，涵盖其核心算法模块（优化、积分、插值、线性代数等）、软件架构与社…
编程语言与软件工程2020 · 387 分 · 98 评入门 · 约 45 分钟编辑精选Lisp 的历史（1979）
History of Lisp (1979)
这是 Lisp 发明者 John McCarthy 于 1979 年为 HOPL（编程语言史）会议撰写的回顾文章，讲述 Lisp 的起源、设计动机与早期演进，文中也涉及 if 表…
编程语言与软件工程2018 · 352 分 · 44 评入门 · 约 45 分钟编辑精选使用 NumPy 进行数组编程
Array Programming with NumPy
这篇 Nature 文章介绍 NumPy 的数组编程模型及其在科学计算中的核心作用：以 ndarray 为中心，通过向量化操作让 Python 高效处理多维数组。
编程语言与软件工程2020 · 318 分 · 134 评入门 · 约 40 分钟编辑精选