dhilst

RSS: https://dhilst.github.io/atom.xml
个人博客。

从不询问任何人的锁：用模型检查器绕过共识

作者用模型检查器（model checker）为一个 NFS 共享锁设计证明其永远不会损坏数据或死锁。背景是一条跨多机的大 pipeline，各机挂载同一 NFS 导出做共享 scratch，写前必须先获取目录锁，读不受限。 关键点是锁本身不跟任何节点通信、不选举、不做心跳，靠形式化方法保证安全性，而非依赖共识协议。文末强调这是"在周二拒绝实现 Raft"之后才得到的方案。 全文偏工程实践，含可在线查看的规范（Caelum 文档），适合关注形式化验证、分布式锁设计、以及不想上 Raft 的团队。讨论点：NFS 上的锁在崩溃/网络分区时的语义边界、model checker 覆盖的假设是否足够、以及把"boring"当设计目标是否真可推广。
评论点赞收藏4 天前

AI 时代，我如何理解软件开发：一个嵌套优化模型

作者把软件开发建模为“嵌套优化”：内层由 AI agent 负责根据报错与测试不断修码、把观察到的失败固化为可执行约束，以提升测试套件“完全性”；外层由人类开发者审查测试是否真正代表需求、修复是否满足意图，以守住“可靠性”（soundness），因为机器只能机械增长覆盖，不能判断行为是否对齐意图。 文中用形式化符号定义版本意图 I_v、代码 C_t、测试 T_t，并引入 soundness/completeness、距离 d(T,E) 等概念，还提出“快/慢测试层”如何把慢层发现的缺陷下沉为快层测试，以及 AI 批量处理 PR 的工作流。 最后给出两个猜想：若 soundness 与 completeness 都趋近 1，运行错误数量应趋近 0；若代码在无人监督下无限膨胀、completeness 趋近 1 而 soundness 趋近 0，则代码库与运行错误都会趋近无穷——即 AI 会不断“自证正确”但逐渐丧失对齐真实意图的能力。 整体偏理论框架，适合对 AI 辅助开发、测试工程与软件可靠性感兴趣的读者。
评论点赞收藏10 天前

AI 时代我如何理解软件开发

作者提出把软件开发看作“嵌套优化”：内层由 AI 代理针对失败和测试不断修代码，外层由开发者修正代理的理解、测试和补丁是否符合作者意图。 核心观点是：大多数软件上线前并没有被证明正确，而是测试到“够用”就发布，生产环境出问题后再修、补测试、再发布。模型用 Iᵥ 表示某版本软件的意图（用户、开发者和业务期望，比写在文档里的规格更大），Cₜ 是 t 时刻代码，Tₜ 是测试集，e 是观察到的错误；当 e 暴露代码违反意图时，内层优化围绕 e 改进代码，外层优化则调整 Iᵥ 的理解、测试与修复策略。 文章强调“意图”比规格更大，很多意图只有在软件违反它时才显现，这一框架试图为 AI 时代的人机协作开发给出可讨论的形式化视角。
评论点赞收藏11 天前

地牢证明爬行者：用RPG游戏学习如何撰写数学证明

一款将数学证明过程转化为RPG游戏机制的作品。玩家需在黎明前深入地下世界击败怪物，而击败怪物的方式是完成它们守护的未竟证明。 该项目基于Algae内核开发，并编译为WebAssembly运行在浏览器中，旨在以互动游戏的形式展示形式化证明的魅力。
评论点赞收藏86 天前

等式推理与归纳法（第一部分）

作者重学形式化方法，在阅读关于代数规范的书籍后，编写了一个名为 algae 的插件来辅助 Claude 进行练习。 作者目前更关注证明的可读性，因此选择了一种显式的语法结构，暂时未深入检查器的正确性问题。
评论点赞收藏108 天前

Caching RPM repositories with Nginx

I’ve been work in a project that requires installation of a huge amount of packages during testing. I usually setup the upstream repostiories, the problem with this is that it keep downloading the sam...
评论点赞收藏282 天前

dlopen will bite you

Meat author: Yes, this post was generated mostly by GPT5, but I’m adding my own notes to make things clearer and funnier. Soo all italic stuff is me (an human) “speaking” Summing up I was trying to ge...
评论点赞收藏374 天前

Fuzz testing in Rust

In this post I explain how I used fuzz testing to catch bugs in a date time parsing library I’m contributing to. Fuzz testing means testing some system with random input data and iterate over mutation...
评论点赞收藏746 天前

Why use Rust? A simple Regex parser example

In this post I show why I would chose Rust over other languages for a project in present date. I do this by using a library for parsing dates as example, exposing strong points of Rust in a real examp...
评论点赞收藏764 天前

How I write React components as state machines

Sometime ago I started working with React again and after some few weeks I already had one of that components with dozens of useState calls. At that point I learned useReducer hook (I already used Red...
评论点赞收藏961 天前

Abstracting recursion over AST

Something that I think is realy useful when working with abstract syntax trees, is the possibility to do tree transformations. Trees transaformations can be used to add information to the AST from a s...
评论点赞收藏982 天前

TCO in Python with exceptions

I was wondering if it would be possible to implement infinite recursion (TCO) in Python by using exceptions to discard the intermediary stack frames, and IT IS POSSIBLE! Here is how, more explanation ...
评论点赞收藏1196 天前

Dependent pairs in Python

Is possible to encode dependent pairs (or sigma types) in python using TypeGuard, abtract classes and subtyping. Dependent pair is a pair of a value and a predicate about that value, in Coq is denoted...
评论点赞收藏1320 天前

Implementing call/cc in Ruby

call/cc is an Scheme function that make it possible to implement all sorts of control flows. From loops to generators, try/catch, green threads, etc. In this post I show a simple implementation of cal...
评论点赞收藏1455 天前

Almost dependent typechecking in Python

In this post I evolve the idea of typechecking Python code by using the ast module introduced at Polymorphic Typechecking in Python by Unification, but instead of using unification I use evaluation to...
评论点赞收藏1518 天前

Dependent Typed Lambda Calculus in Python

In this series of posts I will port this post about dependent typed lambda calculus to Python. This is the third and last one Dependent typed lambda calculus (with tests). I continue from where I stop...
评论点赞收藏1529 天前

Untyped lambda calculus in Python

In this series of posts I will port this post about dependent typed lambda calculus to Python. This is the first type: Untyped lambda calculus (with tests). This code uses functions implemented/explai...
评论点赞收藏1530 天前

Simply Typed Lambda Calculus in Python

In this series of posts I will port this post about dependent typed lambda calculus to Python. This is the second one Simply typed lambda calculus (with tests). I continue from where I stopped in the ...
评论点赞收藏1530 天前

登录芦苇

登录后关注作者、收藏内容和参与讨论。

热门话题

人工智能12,865 人关注AI 会怎样改变日常工作？产品思考8,243 人关注怎样判断一个产品值得长期做？独立开发5,917 人关注一个人如何持续完成作品？
关于芦苇 · 联系我们 · © 2026 芦苇