Hacker News 中文摘要

文章摘要

文章核心内容：作者分享了一个提高编程效率和准确性的技巧，即在编写代码时，在脑海中勾勒出代码功能的证明。这种方法需要大量练习，但一旦掌握，代码往往能在首次或第二次尝试时成功运行。作者还提到，关注代码中的单调性部分有助于更好地理解代码行为。

文章总结

这篇文章主要介绍了一种帮助程序员更快、更准确地编写代码的技巧，即“在编写代码时，同时在脑海中构建代码正确性的证明”。作者将这种技巧称为“微推理”，并分享了几种具体的推理方法，包括单调性、前置和后置条件、不变性、隔离和归纳法。以下是文章的主要内容总结：

1. 单调性（Monotonicity）

单调性指的是代码或数据结构的某些部分只能单向变化，不会“倒退”。例如，检查点（checkpointing）技术就是一个单调性的例子，脚本只能向前推进，不能回退已经完成的步骤。
作者还提到了LSM树（Log-Structured Merge Tree），它是一种在数据库中使用的数据结构，主要通过追加操作来记录插入、删除和更新操作，只有在压缩时才会删除过时的操作，因此具有单调性。

2. 前置和后置条件（Pre- and Post-conditions）

前置条件是指函数执行前必须满足的条件，后置条件是指函数执行后必须满足的条件。通过明确这些条件，可以帮助程序员更好地推理代码的正确性。
作者建议通过明确后置条件来生成单元测试，并在代码中添加断言来确保前置和后置条件的正确性。

3. 不变性（Invariants）

不变性是指代码在运行前、运行中和运行后都必须保持为真的条件。例如，复式记账法中的会计等式就是一个不变性的经典例子，借贷必须始终保持平衡。
作者建议将代码分解为原子步骤，并证明每个步骤都保持不变性，从而确保整个代码的不变性。

4. 隔离（Isolation）

隔离是指在进行代码修改时，确保不影响系统的其他部分。作者提出了“爆炸半径”的概念，即一个修改可能会影响到其他部分，因此需要通过“防火墙”来限制修改的传播。
作者通过一个查询引擎的例子说明了如何通过隔离来确保修改不会引起回归问题。

5. 归纳法（Induction）

归纳法是一种用于处理递归函数和递归数据结构的证明方法。通过归纳法，可以逐步证明代码的正确性，而不需要一次性证明所有情况。
作者通过一个简化树结构的递归函数，展示了如何使用归纳法来证明代码的正确性。

6. 证明亲和性（Proof-affinity）

作者提出了一种衡量代码质量的标准，即“证明亲和性”，指的是代码是否易于推理和证明其正确性。如果代码易于证明，那么它很可能是设计良好的。
作者建议在设计代码时，尽量使其具有单调性、不变性，并明确前置和后置条件，从而提高代码的证明亲和性。

7. 如何提高推理能力

作者认为，这种微推理能力需要通过大量的练习来培养，类似于打字时的肌肉记忆。建议通过编写数学证明、参与算法课程或LeetCode练习来提高逻辑思维能力。

总结：

这篇文章的核心思想是通过在编写代码时进行微推理，程序员可以更快、更准确地确保代码的正确性。作者分享了几种具体的推理方法，并建议通过练习和设计来提高代码的“证明亲和性”。这种方法不仅有助于编写高质量的代码，还能提升程序员对复杂系统的理解能力。

评论总结

以下是评论内容的总结：

主要观点：

代码验证与证明的重要性：
- hiAndrewQuinn 提到二分查找及其变体在编写时容易出错，90%的专业程序员实现中存在bug，强调了循环不变式的重要性。
  - 引用：“Jon Bentley, the writer of Programming Pearls, gave the task of writing an ordinary binary search to a group of professional programmers at IBM, and found that 90% of their implementations contained bugs.”
- nayuki 强调循环不变式和结构归纳是计算机科学证明中的强大技术。
  - 引用：“In addition to pre-conditions and post-conditions, I would like to emphasize that loop invariants and structural induction are powerful techniques in CS proofs.”
代码简洁性与实践：
- gregorygoc 认为编写正确的证明和程序验证很难，建议编写符合语言和代码库习惯的代码，提倡简洁、清晰和通用性。
  - 引用：“Thinking about invariants and pre-post conditions is often unnecessary or greatly reduced if you write idiomatic code for the language and codebase.”
- pclowes 提倡测试驱动开发（TDD），认为每个测试都是一个迷你证明，覆盖了前置/后置条件和不变式。
  - 引用：“When done well, every test you write before you see it fail and then you write the barest amount of code that you think will make it pass is a mini-proof.”
类型系统与证明：
- roadside_picnic 认为类型系统可以看作是小型的定理证明器，使用类型等同于在头脑中编写小证明。
  - 引用：“So more practical type systems can be viewed as ‘little’ theorem provers in the sense the author is describing.”
- bcheung 认为类型本身就是证明，但指出并非所有情况下都需要深入思考每个细节，有时快速交付比编写100%正确的代码更重要。
  - 引用：“When I think of proofs in code my mind goes straight to types because they literally are proofs.”
并发代码的复杂性：
- dblohm7 和 cespare 都提到在编写非平凡的并发代码时，验证代码的正确性尤为重要，尤其是在使用互斥锁或无锁算法时。
  - 引用：“I’ll often ‘fuzz’ the scheduling of multiple tasks around the region of code I’m working on to prove to myself that it works.”
设计与证明的结合：
- thesuperbigfrog 建议在代码中直接包含小证明，提到多种编程语言支持设计契约（Design-by-Contract），如Ada和Rust。
  - 引用：“Why not include little proofs in the code when you can? Several programming languages and libraries support Design-by-Contract.”

其他观点：

ryandv 认为学术计算机科学和数学知识即将过时，大型语言模型可以代替人类进行这些思考。
- 引用：“Why bother thinking through things with your antiquated neural wetware when the computer can do it better, faster, and more correctly?”
wiseowise 认为成为更好的程序员的关键是多编程，少读网上的废话。
- 引用：“To be a better programmer, program more and read less bullshit on the internet.”

总结：

评论中主要讨论了代码验证、证明和简洁性在编程中的重要性，尤其是在处理复杂算法和并发代码时。类型系统和设计契约被视为有效的证明工具，而测试驱动开发则被推荐为实践中的有效方法。尽管有人认为学术知识即将过时，但多数评论者仍强调深入思考和验证代码的必要性。

成为更优秀的程序员，在心中书写简洁证明 -- To be a better programmer, write little proofs in your head