安全与密码学2017blockstream.com
Simplicity：一种面向区块链的新语言
Simplicity: A New Language for Blockchains
专业 · 约 90 分钟读完前置知识：Lambda 演算、形式化验证基础、智能合约基础
导读
这篇论文提出 Simplicity，一种面向区块链的新型编程语言，旨在用可形式化验证的小型语言取代现有智能合约语言，以提升安全性和可证明性。其设计偏向理论化（类似 lambda 演算），强调程序正确性证明而非易用性。
HN 关注点：区块链编程语言的安全性与可验证性，讨论焦点是 Simplicity 是否实用、以及用 Coq 等形式化方法验证合约代码的价值。
HN 评论精选
这几条评论里：支持 2 质疑 1 补充 1
支持区块链是形式化验证工具 Coq 的理想应用场景
这个领域是 Coq 的杀手级应用。没有其他地方 bug 代价如此之高，而程序规模又如此之小。
adamnemecek查看英文原文
This field is a killer app of coq. Nowhere else do your bugs cost more while the program size is small.
补充社区驱动的区块链生态充满势能，长期会产出优秀成果
我喜欢这一切几乎完全由社区开发，没有任何中央权威阻止它朝任何方向发展。（可能有强势玩家在激励某些分支，但对这种东西影响有限。）所以尽管批评者说了很多（我也同意其中一些观点），这件事背后的势能和热情让人感觉 5-10 年内一定会产出真正酷的东西，无论现在人们指出什么问题。
tw1010查看英文原文
What I love about all this is that it is almost entirely developed by the community, without any central authority preventing it from going in any particular direction. (There might be powerful players incentivizing certain branches, but that has limited effect for a thing like this.) So despite what critics say (and I admit to agreeing with them on some points), it just feels like this whole thing has such a momentum and enthusiasm behind it that something really cool will come out of it within 5-10 years, no matter what problems people point out about it at the moment.
质疑Simplicity 过于理论化，程序庞大难读，不适合实际使用
我真的很欣赏作者尝试创造一门新的有价值语言，我自己也在研究这个课题。令我担心的是，这门语言不适合任何实际编程。即使是最简单的智能合约，最终的 Simplicity 程序也会因为缺乏熟悉的数据结构和构造而变得庞大且难以阅读。这门语言让我想起某种 lambda 演算，适合理论研究但不适合实际使用。我不愿意用语言便利性换取更好的可证明性：两者必须同时兼顾，只有那样对最终用户才是合适的。
unboxed_type查看英文原文
I do appreciate the author's attempt to create a new worthy language really, I do a research on this topic myself. What concerns me is that the presented language is not suitable for any practical programming. Even for the most simple smart contracts, the final Simplicity program will be huge and unreadable due to the lack of familiar data structures and constructs. The language resembles me some kind of lambda calculus which is good for theoretical investigation, but not suitable for practical stuff. I am not ready to exchange a language convenience for better provability: it must have both issues addressed at the same time, only then the mix will be right for an end-user.
支持区块链编程需要专门的新语言，Solidity 不够可靠
区块链编程从根本上不同于所有其他编程，我们需要一门新语言来应对这一点。"Solidity" 远谈不上稳固。
tbodt查看英文原文
Blockchain programming is fundamentally different from all other programming, and we need a new language to handle that. "Solidity" is far from solid.
相关资源
从这篇论文所有 HN 讨论帖的全部评论里整理出来的链接。
历次讨论
- 2017Hacker News 讨论帖300 分 · 95 评
同领域还值得读
如何入侵一台已关机的电脑：在 Intel ME 中运行未签名代码
How to hack a turned-off computer, or running unsigned code in Intel ME
这篇 Black Hat 2017 白皮书讨论 Intel Management Engine（ME）的安全问题：如何在 ME 中运行未签名代码，以及攻破处于关机状态的电脑的相关…
安全与密码学2017 · 543 分 · 107 评专业 · 约 40 分钟编辑精选比特币：一种点对点的电子现金系统（2008）
Bitcoin: A Peer-to-Peer Electronic Cash System (2008)
中本聪 2008 年发表的比特币白皮书，提出了无需可信第三方的点对点电子现金系统。
安全与密码学2017 · 536 分 · 394 评入门 · 约 45 分钟编辑精选GPRS 加密算法 GEA-1 的密码分析表明存在故意弱点
Cryptanalysis of GPRS Encryption Algorithms GEA-1 suggest intentional weakness
首次公开了对 GPRS 加密算法 GEA-1 和 GEA-2 的密码分析攻击。
安全与密码学2021 · 487 分 · 107 评专业 · 约 90 分钟编辑精选Signal 消息协议的形式化安全分析
A Formal Security Analysis of the Signal Messaging Protocol
用形式化方法分析 Signal 消息协议（TextSecure）的安全性：作者在多阶段密钥交换模型下，借助自动化证明工具对协议的密钥协商与 Double Ratchet 密钥更新…
安全与密码学2016 · 353 分 · 230 评专业 · 约 120 分钟编辑精选A2：模拟恶意硬件
A2: Analog Malicious Hardware
论文研究如何在芯片设计阶段植入模拟电路形式的恶意硬件后门，使其难以被常规检测发现。
安全与密码学2016 · 315 分 · 94 评专业 · 约 75 分钟编辑精选