编程语言与软件工程2019arxiv.org
Oxide：Rust 的形式化语义
Oxide: A Formal Semantics for Rust
专业 · 约 120 分钟读完前置知识：类型系统与操作语义、Rust 所有权与借用基础、线性代数不需要；建议：简单类型 lambda 演算
导读
这篇论文为 Rust 的一个简化核心方言 Oxide 建立形式化语义，重点刻画所有权与借用，并证明类型系统的基本安全性质（如 progress 与 preservation），从而为 Rust 的内存安全机制提供形式化基础。
HN 关注点：Rust 的形式化基础、论文示例与真实 Rust 的差异，以及这类 PL 研究如何帮助理解真实语言的类型系统与安全性。
HN 评论精选
这几条评论里：质疑 1 补充 2 亲历 1
质疑指出论文示例中的生命周期标注在真实 Rust 中无法直接书写，并讨论显式生命周期声明的限制。
论文里有个例子写的 Rust 代码其实无法通过编译，接近这样：`let msg: &'msg str = "Hello World";`；可以写类似但让编译器推断生命周期：`let msg: &'_ str = "Hello World";`。我在遇到混乱类型问题时经常显式声明类型，但生命周期没那么容易这样写。引入 non-lexical lifetimes 后好一些，但有时仍希望能像第一个例子那样声明生命周期。这个错误示例展示了生命周期的合法用法：链接。
bluejekyll查看英文原文
One of the examples in the paper has some code that you can't actually write in Rust, it's close to this: let msg: &'msg str = "Hello World"; You can write something similar and allow the compiler to infer the lifetime: let msg: &'_ str = "Hello World"; I often find myself declaring the type when I get into confusing type issues in Rust, but you can't do that as easily with lifetimes. With non-lexical lifetimes this has been less of an issue, but still there are times when I would like to be able to declare the lifetime like the first example. This error example shows the valid uses of lifetimes: https://doc.rust-lang.org/nightly/error-index.html#E0261
补充概括 Oxide 是为形式化验证而简化的 Rust 核心，专注所有权与借用。
如果我理解错了请纠正：他们做了一个更简单的 Rust 修改版叫 Oxide，聚焦所有权和借用；这样是为了把它翻译成形式系统，并以容易理解的方式验证。
ipodopt查看英文原文
Please correct me if I am wrong. They produced a simpler modified version of Rust called Oxide that focused on ownership and borrowing. They did did so they could translate it to a formal system and validate it in an easy to understand way.
补充从 PL 语义教学角度说明这类论文的价值，并概述 progress/preservation 与定理证明器的作用。
我在学习编程语言语义，这类论文对理解真实语言的类型系统很有价值，类似 Featherweight Java 和 Featherweight Go。初看内容很多，但从简单类型系统（带类型的算术表达式、简单类型 lambda 演算）入手，会看到同样的定义和元定理反复出现（本文也是）。重复出现的部分包括：语言的项和类型；值（项的子集）；求值关系（如何从一个项走到下一个项）；定型关系（如何构造良类型项及其类型）；Progress：良类型项要么是值，要么可以求值一步；Preservation：良类型项求值一步后仍保持同一类型。口号是 safety = progress + preservation。还应指出，类型系统复杂到一定程度后，肯定想用 Coq 这样的定理证明器做形式验证并自动处理简单情形；证明本身其实相当无聊（这是好事）。
siraben查看英文原文
I'm studying programming language semantics and papers like these are quite valuable in understanding type systems of real languages, see also Featherweight Java[0] and Featherweight Go[1]. At first it looks like a lot to take in, but when you start with far simpler type systems like typed arithmetic expressions and simply-typed lambda calculus, you see the same definitions and metatheorems (properties about the type system) appear over and over again (including in this paper). In particular, the pieces you see repeated are: - the terms and types of the language - the values (a subset of terms) - the evaluation relation, telling you how you go from one term to the next - the typing relation, telling you how you build well-typed terms and what their types are - Progress states that if you have a well-typed term, it either is a value or it can take one step of evaluation - Preservation states you that if you have a well-typed term of type T and it takes a step of evaluation, the resulting term still has type T And we have the slogan, safety = progress + preservation. I should also note that past a certain level of complexity of type system, you definitely would want to use a theorem prover such as Coq to formally verify and automate easy cases. The proofs themselves are actually quite boring (which is a good thing!). [0] https://www.cis.upenn.edu/~bcpierce/papers/fj-toplas.pdf [1] https://arxiv.org/pdf/2005.11710.pdf
亲历亲历 Northeastern 用早期 Rust alpha 授课的 capstone 课程。
很高兴看到 Northeastern 的 PL 研究上新闻！我参加过他们 2015 年的 capstone 课程，当时用/学了刚发布的 Rust alpha 版。很好的经历。
twothumbsup查看英文原文
Love seeing some good PL research from Northeastern in the news! I was part of the capstone class they ran back in 2015 where we used/learned the alpha version of Rust that had just been released. Great experience.
相关资源
从这篇论文所有 HN 讨论帖的全部评论里整理出来的链接。
- 评论区提到的论文
历次讨论
- 2019Hacker News 讨论帖223 分 · 30 评
- 2021Hacker News 讨论帖76 分 · 13 评
同领域还值得读
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 分钟编辑精选