编程语言与软件工程2024arxiv.org编辑精选
将 C 编译为安全 Rust：形式化方法
Compiling C to Safe Rust, Formalized
专业 · 约 90 分钟读完前置知识：形式化验证基础、C 语言语义、Rust 所有权模型
导读
这篇论文研究如何把 C 代码编译为安全的 Rust，并给出形式化方案。从评论看，它主要面向已有形式化验证的 C 代码库，而非典型系统 C，且可能只覆盖 C 的一个受限子集；核心难点在于用 Rust 所有权模型表达真实 C 程序。
HN 关注点：把存量 C 安全迁移到 Rust 的可行性，以及形式化验证前提、C 子集覆盖范围和 Rust 所有权模型适配等现实限制。
HN 评论精选
这几条评论里：质疑 1 补充 2
补充该方法面向形式化验证过的 C，不代表普通系统 C。
值得注意的是，这项工作针对的是“已有的、经过形式化验证的 C 代码库”，这与典型的、未做形式化验证的系统 C 代码有很大不同。
wffurr查看英文原文
Note that this is done for “existing formally verified C codebases” which is a lot different from typical systems C code which is not formally verified.
补充询问与 Zig translate-c 的比较，以及内核为何选 Rust 而非 Zig。
我很好奇它和 Zig 的 translate-c 功能相比如何。Zig 似乎很擅长构建混合环境：新代码用 Zig、旧代码用 C，并支持翻译或互操作，同时自身还是 C 编译器。Linux 内核维护者不把 Zig 当作 C 替代品而选择 Rust，肯定有一些很好的理由。我了解得不够，甚至无法推测，希望有更多知识和经验的人来评价。
zoom6628查看英文原文
I wonder how this compares to the zig-to-C translate function. Zig seems to be awesome at creating mixed environs of zig for new code and C for old, and translating or interop, plus being a C compiler. There must be some very good reasons why Linux kernel maintainers aren't looking to zig as a C replacement rather than Rust. I don't know enough to even speculate so would appreciate those with more knowledge and experiencing weighing in.
质疑质疑 C 子集过小、静态分析受限，且 Rust 所有权模型难匹配真实 C。
那也只是编译 C 的一个极小子集。这个子集可能小到在实践中没什么用。我对这类方法期望很低；它肯定会碰到 C 代码静态分析的能力极限。而且选择 Rust 作为目标会让问题不必要地变难，因为 Rust 的所有权模型与真实 C 程序的工作方式相差太远。
pizlonator查看英文原文
Compiling a tiny subset of C, that is. It might be so tiny as to be useless in practice. I have low hopes for this kind of approach; it’s sure to hit the limits of what’s possible with static analysis of C code. Also, choosing Rust as the target makes the problem unnecessarily hard because Rust’s ownership model is so foreign to how real C programs work.
相关资源
从这篇论文所有 HN 讨论帖的全部评论里整理出来的链接。
历次讨论
- 2024Hacker News 讨论帖291 分 · 157 评
同领域还值得读
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 分钟编辑精选