编程语言与软件工程2018european-lisp-symposium.org
一种 Lisp 方式实现类型论与形式证明（2017）
A Lisp Way to Type Theory and Formal Proofs (2017)
进阶 · 约 45 分钟读完前置知识：Lisp 基础、类型论基础、形式证明/证明助手
导读
这篇论文探讨如何用 Lisp 来表达类型论（type theory）并构造形式化证明，属于把证明助手/证明检查器嵌入 Lisp 生态的尝试。作者 Frédéric Peschanski 后来据此实现了 LaTTe 证明助手；论文本身可见于 2017 年 European Lisp Symposium。
HN 关注点：在 Lisp 里做形式化证明是否可行、与 ACL2 等成熟工业级工具相比如何，以及有哪些入门资料和作者后续实现。
HN 评论精选
这几条评论里：质疑 1 补充 1 亲历 1
质疑质疑论文忽略工业界最成功的 Lisp 证明系统 ACL2，并补充了 ACL2 自验证证明器的相关工作。
看起来不错，但一篇关于 Lisp 与证明的项目居然没提 ACL2？作者有没有调研过 ACL2？如果有，为什么不用它或改进它。ACL2 至今是工业应用最成功的证明系统之一（另一个是 SPIN，TLA+ 现在做类似的事）。至于可信基（TCB），Jared Davis 曾在 x86 处理器上用 ACL2，做了一个朝 ACL2 方向走的逻辑的自验证证明器，并用 Magnus Myreen 的技术一路验证到汇编层。
nickpsecurity查看英文原文
Looks neat but no mention of ACL2 in project about LISP and proving? Come on, now! I wonder if the author investigated it. If so, why not use it or improve it. So far, it's one of most successful in terms of industrial use with SPIN being other one (TLA+ doing similar stuff now). https://www.cs.utexas.edu/users/moore/acl2/ Far as TCB, Jared Davis, who used ACL2 on x86 processors, built a self-verifying prover for a logic going in ACL2's direction. It was verified to assembly using Magnus Myreen's techniques. https://www.cs.utexas.edu/~jared/milawa/Web/
补充推荐一本类型论与形式证明的教材作为延伸阅读。
文中提到的那本书非常好，如果你对这类东西感兴趣值得一读，Kindle 上也有。
tluyben2查看英文原文
The book[0] mentioned is excellent if you are interested in this kind of thing. It is available on Kindle too. [0] https://www.cambridge.org/core/books/type-theory-and-formal-proof/0472640AAD34E045C7F140B46A57A67C
亲历作者本人现身，给出演讲视频和 LaTTe 实现仓库。
我是作者。如果你感兴趣，我在 EuroClojure 2016 讲过类型论，视频在这里：https://m.youtube.com/watch?v=5YTCY7wm0Nw …… 内容其实并不特定于 Clojure，除非你想试试 LaTTe：https://github.com/latte-central/LaTTe
fredokun查看英文原文
Author here. If you are interested I talked about type theory at euroclojure'16. The video is there: https://m.youtube.com/watch?v=5YTCY7wm0Nw ... And it's not really clojure-specific except if you want to try LaTTe: https://github.com/latte-central/LaTTe
相关资源
从这篇论文所有 HN 讨论帖的全部评论里整理出来的链接。
历次讨论
- 2018Hacker News 讨论帖183 分 · 16 评
同领域还值得读
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 分钟编辑精选