一个程序员的心路历程
Go 代码也能像数学定理一样被证明？AI 编程时代，形式化验证正在补上最后一块拼图
当 AI 可以在几分钟内生成大量代码，软件工程真正稀缺的能力可能不再是实现功能，而是证明实现满足要求。本文从 AI 生成代码的验证难题出发，介绍 Gobra 与 Viper 的技术架构，通过完整的 Go 示例拆解契约式验证、循环不变量和并发权限推理，并简要比较 VeGo、Rust 的 Verus 等相关探索，讨论形式化验证如何进入 AI 软件工程流水线，以及它距离大规模生产落地还有多远。
大厨、厨房与餐馆：一文彻底搞懂 AI Agent 背后的“Harness”到底是什么
本文永久链接 – https://tonybai.com/2026/10/24/what-is-a-harness 大家好，我是Tony Bai。 随着以 Claude Code、Cursor 为代表的各类 AI 编程助手与 Agent（智能体）工具的爆发式普及，一个名为“Harness” 的概念在海外技术圈引发了广泛的讨论与争议。很多人好奇：大模型本身、我们使用的客户端界面，以及背后真正驱动工具执行的 Harness，到底各自承担了什么角色？ ...
Go 紧急发布两个安全版本！一次 CA 证书信任危机，暴露 HTTPS 安全体系的薄弱环节
Go 因为一批中间 CA 证书的安全问题，紧急发布 Go 1.26.10 和 Go 1.27.3。本文深入解释这次安全修复的技术原理、证书链信任机制与工程影响，并通过可运行的 Go 示例说明如何验证证书链、排查生产环境中的旧二进制，以及建立更可靠的 Go 安全更新流程。
深入理解 Go 与 SIMD：从底层硬件指令到编译器实现原理
长期以来在 Go 中使用 SIMD 只能依赖繁琐的手写汇编，而 Go 1.26/1.27 引入的实验性 simd 与 simd/archsimd 包彻底打破了这一壁垒。本文深入剖析现代 CPU 向量寄存器与通道（Lanes）的物理机理，详解底层架构包与可移植包的设计权衡，揭秘编译器内建函数（Intrinsics）与 midway 多重编译的底层黑魔法，并通过广播、融合乘加（FMA）、掩码混合与尾部处理等核心操作，手把手构建跑出 9 倍性能飞跃的点积计算实战，为 Go 开发者提供了一套完整的硬件向量化加速指南。
Go 并发的天花板，被一个 30 年前的老模型捅破了？CML 把 channel 玩出了新花样
Go 的 select 只能在语句里描述通信，无法封装复用。Concurrent ML (CML)把通信操作做成可传递、可组合的“事件值”，让选择、超时、取消统一在同一套抽象里，并让阻塞线程可被垃圾回收。本文结合 Racket 与 Go 代码，梳理 CML 相对 Go 的三大优势，并给出 Go 开发者可以立即采用的思路。