结构化编程诞生于可推导性追求，goto有害的真正原因

Dijkstra最初的目标不是”消灭goto”，而是想让程序员能像数学家一样用公理、定理、推论构成的欧几里得结构去证明程序正确性——把程序递归拆分成一个个可证明的小单元，只要每个单元被证明正确，就能推导出整个程序的正确性。他发现goto语句的某些用法会破坏这种递归拆分能力，让模块无法被分解成更小的、可证明的单元；而goto的其他用法虽不破坏可证明性，但效果和更简单的if-then-else分支结构、do-while循环结构完全一致。恰逢Böhm和Jacopini证明了顺序结构、分支结构、循环结构这三种结构足以构造出任何程序——这个发现的关键意义在于：构建可推导模块所需要的控制结构集合，与构建所有程序所需要的最小控制结构集合完全等同。这就是[[三大编程范式的共性是各自移除一种编程能力而非增加]]里结构化编程”限制程序控制权直接转移”这句总结的真正来源：不是随意的语法洁癖，而是”只有去掉无限制跳转，程序才能被递归分解成可证明单元”这一数学事实的直接推论。顺序结构的正确性可用枚举法证明，分支结构靠枚举每条路径，循环结构则需要数学归纳法（先证循环1次正确、再证N次正确则N+1次也正确、最后证起止条件）——这套证明体系虽完备但极其繁琐，为后续”形式化证明最终没有普及”埋下了伏笔。