传统的临界区策略，不能从语法层面杜绝劣质代码绕过资源锁。采用临界区设计多线程算法，防止资源冲突，完全凭程序员自觉地采用临界区机制。可能因一时马虎，铸成大错。
chan 通道，要求使用数据的代码必须先从通道取得资源，然后才有可能继续访问资源。这个机制从语法层面防止了资源访问冲突。
当然，这是我最初的感悟。
程序正确性证明因工作需要，重构一套旧的 C 语言编写的激光摄像机联动程序。原来的代码中用到了 7 个全局变量，其中有 3 个变量可能在硬件中断程序中被修改。
在代码评审时我忽然发现，由于业务逻辑中的变量数值随时可能在别的“线程”中修改，这导致一个严重问题 —— 代码正确性很难从数学角度加以证明。按照形式化软件工程学的理论，一个零缺陷的程序在设计完成后，需要进行“验证”和“测试”，也就是英文说的 Verification 和 Test。
如果采用传统的临界区策略（事实上，嵌入式 C 语言连临界区也不支持），很难做 Verificatuion。
我发现 Haskell、Erlang 这类函数式程序设计语言，都是采用了通道来锁定资源，利用通讯共享数据，最根本的原因，就是确保代码的“可验证性”。代码的“可验证性”，参见形式化软件工程方面的书籍。