让代码更可靠的小技巧:边写代码边证明它能正确运行


让你的代码更可靠?秘诀是在脑中“写证明”!

有网友分享了一个写代码时的小技巧,引发了大量程序员的共鸣。这个技巧就是:边写代码边在脑中“证明”它会正确运行

这是一个技巧,但其实更像一种思维习惯:在写每一行代码的同时,不断验证它的逻辑是否自洽、是否会出错。当这种思维方式练熟之后,很多人会惊喜地发现:自己的代码常常一次就能跑通,甚至无需调试。

具体如何“证明”呢?Matthew提供了五个实战中常用的思路:

  1. 单调性

程序中的某些状态一旦更新,就不该回退,比如“已完成的任务”“增长的日志”等。想象某个状态只能往一个方向变化,就能排除很多可能出错的路径。

  1. 前置条件 / 后置条件

明确函数“执行前必须成立”和“执行后必须成立”的条件,从而帮助你设计测试用例 & 写断言。如果某个函数的前/后置条件说不清楚,说明它本身就写得不清楚,值得重构!

  1. 不变量

不变量是贯穿整个程序生命周期必须保持不变的条件。把程序拆成小步骤,每一步都必须守住这个不变量,整体自然可靠。

当你发现系统变得诡异或时好时坏时,往往是某个关键不变量被偷偷破坏了。

  • 隔离变化

代码的每一次改动,都有一个“爆炸半径”。理想情况下,变化应尽量局限在本模块内部,而不是牵一发而动全身。

可以利用模块边界或接口作为防火墙,贯彻“开闭原则”:加功能是加代码,而不是改旧代码。

  • 归纳法

当你面对递归结构(比如树、列表)或写递归函数时,用数学归纳思维最自然。先证明最简单情况是正确的。再假设子结构已经正确,然后证明更大结构也正确。

作者在文章最后一段抛出了一个核心概念:Proof-affinity,直译是“可证明性”。

简单来说就是,你写的代码,能不能轻松地用逻辑说服自己它不会出错。

不依赖测试、不需要日志,只靠逻辑推导,你就能大致确信这段逻辑的正确性,这种代码往往设计得很优秀。

上述的这些技巧,不仅能帮助你推理,也能反过来指导你如何写出好代码。换句话说:能被“证明”得越轻松的代码,往往本身就设计得更好。

这种证明的能力和练习打字一样,需要反复练手、变成本能。作者推荐从这三件事做起:

  • 多写数学证明

  • 多刷Leetcode,但重质不重量

  • 尝试用证明的方式解释自己的代码逻辑

感兴趣的朋友可以查看原文:https://the-nerve-blog.ghost.io/to-be-a-better-programmer-write-little-proofs-in-your-head/


相關推薦

2023-12-05

"代码的阅读胜于编写"这句话现在已经是程序员共识,它提醒我们,在编写代码时不能仅追求方便,而忽视那些将来需要阅读和修改代码的人。更一般地说,"代码的阅读胜于编写"传达了一个观点:通过保持代码可维护性,保持

2023-04-24

念, 一个好的软件, 不仅仅只是内存安全和绝对性能, 代码可读性, 场景适合性, 认知深刻和持续维护的软件对用户才有价值, 重写完一个软件, 证明 rust 比别的语言快和自己厉害, 马上就弃坑的软件没有价值。 3. Rust社

2022-12-04

口现在可与 Anaconda 软件包库配合使用,让您可以在编写代码期间直接自定义 Conda 解释器。 通过设置使用新 PyCharm UI 切换到新 UI,预览 PyCharm 完全重做的外观。 勾选 Settings/Preferences | Appearance & Behavior(设置/偏好设置 | 外

2023-05-27

开发者之间一些重复的审计工作。 “Rust 可以轻松地将代码封装和共享到 crate 中,crate 是可重用的软件组件,就像其他语言中的包一样。我们拥抱广泛的开源 Rust crate 生态系统,既利用了谷歌以外编写的 crates,也发布了我们自

2025-03-22

个福音。   二、一键可达同类应用列表 接下来的小技巧,必须要敲黑板了!首先新版本的AppGallery在应用页增加了腰部分类胶囊的模块,提供了超过20个分类胶囊,大家可以通过滑动选择感兴趣的胶囊,找到同类型应用

2023-11-28

声称在 shutdown 过程中拥有"优先权",并且在确保设计可靠且能妥善解决实际问题方面存在其他障碍,那么具体的实现就会存在一些困难。 目前为止,大家对这种方法的意见还很不统一。现阶段能否设计出一种既能为主线所

2025-06-07

ChatGPT 3.5 诞生以来,越来越多的个人和企业将 LLM 生成的代码融入日常开发与自动化。然而,实践证明:LLM 生成的代码虽然“看起来没问题”,却常因对底层语言细节把握不准导致微妙 Bug——比如运算符优先级混淆、作用域处

2023-05-10

性和机密性的核心安全属性,将证明扩展到内核的二进制代码,并对一个 protected mode OS 进行了首次健全和完整的最坏情况下的执行时间分析。 seL4 高可靠微内核从根本上改变了研究界对形式化方法所能完成的认识:它表明不仅

2023-01-04

搞定了 Win 64 和 Linux x64 版本的脚本,并且还有余力进行代码优化。 极具“开源”精神的他更是直接将贡献热度的工具开源了出来:https://gitee.com/maikebing/oschina2022 “热度值”是评选「最火热中国开源项目社区」的核心指标,

2023-04-02

验。以下是关于 NGPTLT++ 整合 GPT-4 特点的部分: 自动代码生成:借助 GPT-4 的强大生成能力,NGPTL++ 可以根据程序员的需求和描述自动生成相应的代码片段。这大大减轻了程序员的编程负担,提高了开发效率。 代码优化:NG

2025-07-23

8种外语互译、9种外语识别。 在交互设计上,X5支持边录边写功能,录音转写时可同步手写,会后回顾支持回听回看、即点即读。安全防护方面,设备配备物理离线拨键与微孔指示灯,一键开启后隔绝所有网络连接;笔记保密箱

2025-04-16

核心目标明确:为构建Agent应用的开发者提供更强悍、更可靠且更经济的基础设施。 值得关注的是,由于GPT-4.1 更严格、更字面地遵循指令,会非常严格地按照字面指令去执行任务。这使得它对明确、清晰的提示尤其敏感。 也

2025-07-22

合不同来源的硬件与算法库,就像一场永无止境的“胶水代码”战争。 分布式难题: 多机器人协作时,通信冲突、带宽抢占等问题层出不穷。 我们相信,是时候用现代化的软件开发实践,为机器人领域带来一些改变了。 Do

2024-11-01

pt 原有语法的基础上,ArkTS 加强了静态检查,从而提高了代码的质量和性能。同时,它还增强了并发编程的 API,解决了 JavaScript/TypeScript 在并发能力上的不足。此外,ArkTS 支持与 JavaScript/TypeScript 的高效互操作,保证了生态的兼