编程语言与软件工程2016goto.ucsd.edu
Liquid Haskell：将 Haskell 作为定理证明器
Liquid Haskell: Haskell as a Theorem Prover
专业 · 约 120 分钟读完前置知识：Haskell 类型系统、SMT 求解器基础、形式化验证基础
导读
这篇博士论文研究 Liquid Haskell：将精化类型引入 Haskell，使程序员能在类型中写出逻辑约束（如“函数只返回偶数”“输入必须有序”），由 SMT 求解器在编译期自动验证，从而把 Haskell 变成一个半自动定理证明器。论文还展示了如何用精化类型实现编译期单元测试和断言检查。
HN 关注点：是因为精化类型让普通程序员无需学习完整定理证明就能在编译期验证程序性质，讨论围绕入门资料和底层原理展开。
后来怎么样
Liquid Haskell 成为 Haskell 生态中广泛使用的程序验证工具，精化类型方法也影响了后续在动态语言和系统编程语言中的验证研究。
HN 评论精选
这几条评论里：支持 1 补充 3
支持推荐交互式教程并举例说明精化类型能验证的性质
有一个交互式教程 [1]。我觉得这非常了不起。用精化类型可以声明/证明诸如：这个函数只返回偶数；这个函数的输入不只是任意向量，必须是有序向量；还可以做编译期单元测试——写一个测试代码的函数，测试通过返回 True，再给该函数加上“必须恒为 True”的精化类型，剩下的交给定理证明器。[1] http://ucsd-progsys.github.io/liquidhaskell-tutorial/02-logic.html#/examples-arithmetic
airesQ查看英文原文
There is an interactive tutorial at [1]. I find this quite amazing. With refinement types one can say/prove things like: - This function only returns even numbers. - The input for this function is not just any vector, it must be an ordered vector. - It's possible to make compile time unit tests. Where we write a function that exercises the code, and returns True if the test succeeds. Then one adds a refinement type saying that the function must always evaluate to true. The theorem prover does the rest. [1] - http://ucsd-progsys.github.io/liquidhaskell-tutorial/02-logic.html#/examples-arithmetic
补充补充作者的演讲视频
论文作者 Niki Vazou 的演讲：https://www.youtube.com/watch?v=LEsEME7JwEE
primodemus查看英文原文
Talk by Niki Vazou, the author of the dissertation: https://www.youtube.com/watch?v=LEsEME7JwEE
补充推荐无需 Haskell 背景的入门博客
最早的一篇博客 [1] 提供了很好的、无行话无数学的入门介绍，不懂 Haskell 也能看懂。文中展示的 assert 函数非常酷：定义一个能在编译期检查断言（比如某物不为 null）的函数竟如此容易，这就是入门课级别的代码契约。[1] http://goto.ucsd.edu/~rjhala/liquid/haskell/blog/blog/2013/01/01/refinement-types-101.lhs/
bbcbasic查看英文原文
The very first blogpost http://goto.ucsd.edu/~rjhala/liquid/haskell/blog/blog/2013/01/01/refinement-types-101.lhs/ gives a very nice jargon and maths-free introduction to this. You don't need to know Haskell to follow it really. The assert function shown in the post is really cool. Amazing how easy it is to define a function that will compile time check an assertion (e.g. something is not "null"). That's code contracts done in the 101 class.
补充补充底层原理及精化类型在多个领域的延伸研究
想了解 Liquid Types 式精化类型的底层原理，可以读 Pat Rondon 的博士论文 [链接]。UCSD 程序系统实验室还把精化类型应用到了动态语言和系统编程语言；MIT CAP 组用类似技术做程序合成，普渡的一个组则在研究用机器学习处理难以手工陈述或推断的复杂精化类型。[附多个论文链接]
mkawa查看英文原文
If you'd like to learn more about how the Liquid Types style of refinement types works under the covers, I invite you to read Pat Rondon's thesis: http://goto.ucsd.edu/~pmr/papers/rondon-liquid-types.pdf The UCSD Programming Systems lab has also applied refinement types to dynamic languages[1] and systems programming languages[2]. The MIT Computer Assisted Programming Group has similarly used liquid types-based techniques for program synthesis[3], while a group at Purdue has been working on maching learning of complex refinement types[4,5] that are difficult to state or infer using the liquid types techniques. [1] http://goto.ucsd.edu/~pvekris/docs/pldi16.pdf [2] http://goto.ucsd.edu/~rjhala/papers/low_level_liquid_types.pdf [3] http://people.csail.mit.edu/polikarn/publications/pldi16.pdf [4] https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/icfp_my_version.pdf [5] https://www.cs.purdue.edu/homes/zhu103/pubs/pldipaper.pdf
相关资源
从这篇论文所有 HN 讨论帖的全部评论里整理出来的链接。
历次讨论
- 2016Hacker News 讨论帖199 分 · 26 评
同领域还值得读
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 分钟编辑精选