让你的代码更可靠？秘诀是在脑中“写证明”！
有网友分享了一个写代码时的小技巧，引发了大量程序员的共鸣。这个技巧就是：边写代码边在脑中“证明”它会正确运行。
这是一个技巧，但其实更像一种思维习惯：在写每一行代码的同时，不断验证它的逻辑是否自洽、是否会出错。当这种思维方式练熟之后，很多人会惊喜地发现：自己的代码常常一次就能跑通，甚至无需调试。
具体如何“证明”呢？Matthew提供了五个实战中常用的思路：
程序中的某些状态一旦更新，就不该回退，比如“已完成的任务”“增长的日志”等。想象某个状态只能往一个方向变化，就能排除很多可能出错的路径。
明确函数“执行前必须成立”和“执行后必须成立”的条件，从而帮助你设计测试用例 & 写断言。如果某个函数的前/后置条件说不清楚，说明它本身就写得不清楚，值得重构！
不变量是贯穿整个程序生命周期必须保持不变的条件。把程序拆成小步骤，每一步都必须守住这个不变量，整体自然可靠。
当你发现系统变得诡异或时好时坏时，往往是某个关键不变量被偷偷破坏了。
代码的每一次改动，都有一个“爆炸半径”。理想情况下，变化应尽量局限在本模块内部，而不是牵一发而动全身。
可以利用模块边界或接口作为防火墙，贯彻“开闭原则”：加功能是加代码，而不是改旧代码。
当你面对递归结构（比如树、列表）或写递归函数时，用数学归纳思维最自然。先证明最简单情况是正确的。再假设子结构已经正确，然后证明更大结构也正确。
作者在文章最后一段抛出了一个核心概念：Proof-affinity，直译是“可证明性”。
简单来说就是，你写的代码，能不能轻松地用逻辑说服自己它不会出错。
不依赖测试、不需要日志，只靠逻辑推导，你就能大致确信这段逻辑的正确性，这种代码往往设计得很优秀。
上述的这些技巧，不仅能帮助你推理，也能反过来指导你如何写出好代码。换句话说：能被“证明”得越轻松的代码，往往本身就设计得更好。
这种证明的能力和练习打字一样，需要反复练手、变成本能。作者推荐从这三件事做起：
多写数学证明
多刷Leetcode，但重质不重量
尝试用证明的方式解释自己的代码逻辑
感兴趣的朋友可以查看原文：https://the-nerve-blog.ghost.io/to-be-a-better-programmer-write-little-proofs-in-your-head/
评论删除后，数据将无法恢复
让代码更可靠的小技巧：边写代码边证明它能正确运行
让你的代码更可靠？秘诀是在脑中“写证明”！
有网友分享了一个写代码时的小技巧，引发了大量程序员的共鸣。这个技巧就是：边写代码边在脑中“证明”它会正确运行。
这是一个技巧，但其实更像一种思维习惯：在写每一行代码的同时，不断验证它的逻辑是否自洽、是否会出错。当这种思维方式练熟之后，很多人会惊喜地发现：自己的代码常常一次就能跑通，甚至无需调试。
具体如何“证明”呢？Matthew提供了五个实战中常用的思路：
程序中的某些状态一旦更新，就不该回退，比如“已完成的任务”“增长的日志”等。想象某个状态只能往一个方向变化，就能排除很多可能出错的路径。
明确函数“执行前必须成立”和“执行后必须成立”的条件，从而帮助你设计测试用例 & 写断言。如果某个函数的前/后置条件说不清楚，说明它本身就写得不清楚，值得重构！
不变量是贯穿整个程序生命周期必须保持不变的条件。把程序拆成小步骤，每一步都必须守住这个不变量，整体自然可靠。
当你发现系统变得诡异或时好时坏时，往往是某个关键不变量被偷偷破坏了。
代码的每一次改动，都有一个“爆炸半径”。理想情况下，变化应尽量局限在本模块内部，而不是牵一发而动全身。
可以利用模块边界或接口作为防火墙，贯彻“开闭原则”：加功能是加代码，而不是改旧代码。
当你面对递归结构（比如树、列表）或写递归函数时，用数学归纳思维最自然。先证明最简单情况是正确的。再假设子结构已经正确，然后证明更大结构也正确。
作者在文章最后一段抛出了一个核心概念：Proof-affinity，直译是“可证明性”。
简单来说就是，你写的代码，能不能轻松地用逻辑说服自己它不会出错。
不依赖测试、不需要日志，只靠逻辑推导，你就能大致确信这段逻辑的正确性，这种代码往往设计得很优秀。
上述的这些技巧，不仅能帮助你推理，也能反过来指导你如何写出好代码。换句话说：能被“证明”得越轻松的代码，往往本身就设计得更好。
这种证明的能力和练习打字一样，需要反复练手、变成本能。作者推荐从这三件事做起：
多写数学证明
多刷Leetcode，但重质不重量
尝试用证明的方式解释自己的代码逻辑