May 2026

All Articles - 91
2026
复刻多 Agent 诊断系统：47 个失败模式复盘
复刻多 Agent 诊断系统：47 个失败模式复盘
附录：Curry-Howard-Lambek 三角，范畴论第三条腿
附录：Curry-Howard-Lambek 三角，范畴论第三条腿
收束：作为日常工具的形式化
收束：作为日常工具的形式化
形式化方法的局限与工程取舍
形式化方法的局限与工程取舍
大型形式化案例：CompCert、seL4、Four Color 与 Mathlib
大型形式化案例：CompCert、seL4、Four Color 与 Mathlib
从一个 git 仓到 Skill Hub：一道全栈架构题的逐层推导
从一个 git 仓到 Skill Hub：一道全栈架构题的逐层推导
类型检查器的可信基底：编译通过到底信什么
类型检查器的可信基底：编译通过到底信什么
在 Lean 4 中证明经典命题
在 Lean 4 中证明经典命题
准备 Lean 4 实验环境
准备 Lean 4 实验环境
归纳类型与递归：把数据嵌入证明
归纳类型与递归：把数据嵌入证明
依值类型：从命题逻辑到一阶逻辑
依值类型：从命题逻辑到一阶逻辑
类型检查算法：证明检查算法的机械实现
类型检查算法：证明检查算法的机械实现
简单类型 lambda 演算：最小可证明系统
简单类型 lambda 演算：最小可证明系统
命题即类型：Curry-Howard 同构
命题即类型：Curry-Howard 同构
直觉主义逻辑与 BHK 解释：什么算一个证明
直觉主义逻辑与 BHK 解释：什么算一个证明
编译通过为什么就是定理得证：形式化方法系列导引
编译通过为什么就是定理得证：形式化方法系列导引
U型思考法：从表象到本质的深度思维模型
U型思考法：从表象到本质的深度思维模型
情绪提示词：用心理学手段提升 LLM 性能的研究综述
情绪提示词：用心理学手段提升 LLM 性能的研究综述
回到工程：Linux VM 如何改变性能诊断
回到工程：Linux VM 如何改变性能诊断
OOM Killer：内核什么时候决定杀进程
OOM Killer：内核什么时候决定杀进程
cgroup memory：内存从全局资源变成局部预算
cgroup memory：内存从全局资源变成局部预算
SLUB：小对象为什么不直接按页分配
SLUB：小对象为什么不直接按页分配
Buddy system：物理页如何按阶分配
Buddy system：物理页如何按阶分配
Huge Page：TLB 压力和页表开销
Huge Page：TLB 压力和页表开销
NUMA：内存为什么有远近
NUMA：内存为什么有远近
Swap：换出去的页怎样回来
Swap：换出去的页怎样回来
页回收：kswapd 和 direct reclaim
页回收：kswapd 和 direct reclaim
LRU 和 workingset：内核如何近似"最近使用"
LRU 和 workingset：内核如何近似"最近使用"
反向映射：从物理页找回虚拟地址
反向映射：从物理页找回虚拟地址
Folio：为什么内核重新组织 page 抽象
Folio：为什么内核重新组织 page 抽象
文件映射和 page cache：文件内容怎样变成页面
文件映射和 page cache：文件内容怎样变成页面
匿名页和 COW：fork 为什么便宜，写入为什么变贵
匿名页和 COW：fork 为什么便宜，写入为什么变贵
缺页异常：一次访问如何进入内核
缺页异常：一次访问如何进入内核
页表：CPU 能读懂的翻译结构
页表：CPU 能读懂的翻译结构
地址空间不是数组：mm_struct 和 vm_area_struct
地址空间不是数组：mm_struct 和 vm_area_struct
密码学签名全景：从 HMAC 到数字签名的完整图谱
密码学签名全景：从 HMAC 到数字签名的完整图谱
重读 Linux VM：给系统研究生的虚拟内存导读
重读 Linux VM：给系统研究生的虚拟内存导读
Self-Improving Agent 的边界：外部记忆能不能 shadow 模型权重？
Self-Improving Agent 的边界：外部记忆能不能 shadow 模型权重？
LLM Harness 路线图：从抽卡模型到可验证工程系统
LLM Harness 路线图：从抽卡模型到可验证工程系统
AI 不会吞掉软件，只会吞掉入口
AI 不会吞掉软件，只会吞掉入口
Agent Teams 为什么有效
Agent Teams 为什么有效
环境可供性：智能的一半是取到正确数据
环境可供性：智能的一半是取到正确数据
上下文换入换出：下一代 scaling
上下文换入换出：下一代 scaling
裸模型为什么像抽卡
裸模型为什么像抽卡
Harness 的本质：把随机模型锁进可验证的箱体
Harness 的本质：把随机模型锁进可验证的箱体
AI 编程让人类更累——从 Vibe Coding 到 Brain Fry 的认知负荷真相
AI 编程让人类更累——从 Vibe Coding 到 Brain Fry 的认知负荷真相
回到工程：计算理论怎样改变写代码的眼光
回到工程：计算理论怎样改变写代码的眼光
抽象解释：用保守近似理解程序
抽象解释：用保守近似理解程序
停机问题：为什么某些判断没有通用程序
停机问题：为什么某些判断没有通用程序
通用性：一种机器怎样模拟另一种机器
通用性：一种机器怎样模拟另一种机器
不用数字也能计算：Church 编码
不用数字也能计算：Church 编码
写一个 lambda 规约器
写一个 lambda 规约器
lambda 演算入门：函数为什么足够表达计算
lambda 演算入门：函数为什么足够表达计算
用 Python 写一台图灵机
用 Python 写一台图灵机
图灵机：纸带、读写头和最小通用计算
图灵机：纸带、读写头和最小通用计算
下推自动机：多一只栈就能处理嵌套
下推自动机：多一只栈就能处理嵌套
正则表达式如何变成自动机
正则表达式如何变成自动机
非确定性有限自动机：一次保留多个可能世界
非确定性有限自动机：一次保留多个可能世界
确定性有限自动机：状态、输入和接受条件
确定性有限自动机：状态、输入和接受条件
Harness 也开始进化：复旦 AHE 与可观测性驱动的自演化
Harness 也开始进化：复旦 AHE 与可观测性驱动的自演化
进程启动期的静默故障：JVM 与 Node.js 的调试方法论
进程启动期的静默故障：JVM 与 Node.js 的调试方法论
指称语义：把程序翻译成 Python 函数
指称语义：把程序翻译成 Python 函数
小步语义：把程序执行拆成一步一步的规约
小步语义：把程序执行拆成一步一步的规约
自己写一个解释器：大步语义与递归求值
自己写一个解释器：大步语义与递归求值
程序先变成语法树：从字符串到 AST
程序先变成语法树：从字符串到 AST
刚好够用的 Python：为《计算的本质》准备实验语言
刚好够用的 Python：为《计算的本质》准备实验语言
重读《计算的本质》：给 Java 程序员的可计算性入门
重读《计算的本质》：给 Java 程序员的可计算性入门
AgentScope 全景实战：设计速读与生产级十二层装配
AgentScope 全景实战：设计速读与生产级十二层装配
MyBatis 内部架构深度解析：从 Mapper 方法到 JDBC 执行链
MyBatis 内部架构深度解析：从 Mapper 方法到 JDBC 执行链
Harness Engineering：长程 Agent 的工程化底座
Harness Engineering：长程 Agent 的工程化底座
Agent 全景指南：从必要性、范式演化到高可用落地
Agent 全景指南：从必要性、范式演化到高可用落地
模块化与动态加载的跨平台对照：从 ClassLoader 到 BEAM、ALC、dlmopen
模块化与动态加载的跨平台对照：从 ClassLoader 到 BEAM、ALC、dlmopen
Spring AI 深度：把 LLM 抽象成新一代 JDBC（兼论 LangChain4j 与 Java 智能体框架路线）
Spring AI 深度：把 LLM 抽象成新一代 JDBC（兼论 LangChain4j 与 Java 智能体框架路线）
从 Java 8 到 Java 25 的迁移与 Spring 升级指南
从 Java 8 到 Java 25 的迁移与 Spring 升级指南
从 OSGi 到 Jigsaw：Java 模块化、SPI 与类加载器切换
从 OSGi 到 Jigsaw：Java 模块化、SPI 与类加载器切换
大语言模型为什么像人在说话和思考：语言能力、思考能力与可解释性边界
大语言模型为什么像人在说话和思考：语言能力、思考能力与可解释性边界
递归语言模型 RLM 推理范式深读
递归语言模型 RLM 推理范式深读
用 Skill 和 Agent 攻克老旧历史项目的学习与分析难题
用 Skill 和 Agent 攻克老旧历史项目的学习与分析难题
缓存系统设计全景——从原理到生产的完整指南
缓存系统设计全景——从原理到生产的完整指南
Multi-Agent 架构深度研究：从四种基础模式到「何时不该用多 Agent」的工程判断
Multi-Agent 架构深度研究：从四种基础模式到「何时不该用多 Agent」的工程判断
Context7 MCP Server 深度解析：AI 编程助手的实时文档检索引擎
Context7 MCP Server 深度解析：AI 编程助手的实时文档检索引擎
oh-my-claudecode vs oh-my-openagent：两大 Agent 编排框架深度对比与实用教程
oh-my-claudecode vs oh-my-openagent：两大 Agent 编排框架深度对比与实用教程
Goal 模式深度研究：从 Ralph Loop 到 Codex Runtime、Claude Judge 与 SDD Sidecar
Goal 模式深度研究：从 Ralph Loop 到 Codex Runtime、Claude Judge 与 SDD Sidecar
到底什么是多模态模型
到底什么是多模态模型
中美两国实际社会总债务是多少
中美两国实际社会总债务是多少
OpenCode 自研 SDD 流程注入方案
OpenCode 自研 SDD 流程注入方案
超成本 / 不起量 / 炸量：广告投放线上异常问题全景
超成本 / 不起量 / 炸量：广告投放线上异常问题全景
短事务与高并发缓存初始化
短事务与高并发缓存初始化
CPX / OCPX / eCPM：广告计费家族的全景图与演进版图
CPX / OCPX / eCPM：广告计费家族的全景图与演进版图
如何写好 AGENTS.md
如何写好 AGENTS.md
欧尔班败选与世界大国态度
欧尔班败选与世界大国态度
avatar
magicliang
关于技术以及人生
Articles
512
Tags
575
Categories
10
Github
Announcement
人生只是，守株待兔
Recent Posts
AI 是放大器不是方向：读 Adam Bender 谈软件生态学的 10 倍时刻
AI 是放大器不是方向：读 Adam Bender 谈软件生态学的 10 倍时刻
CI/CD 方法论的前世今生
CI/CD 方法论的前世今生
MySQL 经典架构模式：从主从复制到分库分表
MySQL 经典架构模式：从主从复制到分库分表
Elasticsearch 经典架构模式：从时序索引到跨集群检索
Elasticsearch 经典架构模式：从时序索引到跨集群检索
深入 Elasticsearch（17）：两种搜索引擎的设计选择
深入 Elasticsearch（17）：两种搜索引擎的设计选择
Categories
Tags
影评杨幂诺兰JVMJava异常处理区块链HyperledgerCorda私有链联盟链共识算法javacJIT字节码性能优化科幻DockerSocketJavaScriptKOA数据库MySQLMariaDBLinux虚拟化hypervisorgithubhexo互联网金融FinTechPython面向对象编程语言编程范式操作系统tagGovim体系结构
Archives
Website Info
Article Count :
512
Total Word Count :
2813.2k
Unique Visitors :
Page Views :
Last Update :