Remy

我们必须知道 – 我们将会知道

Hilbert 程序的两项目标（构造完备且一致的公理系统、设计可判定任意数学命题真假的算法）分别被 Gödel 不完备定理和 Turing 停机问题证明不可能实现。

作者指出，AI 智能体如今正把这些目标以形式化证明助手（如 Lean）的形式重新实现，但其影响比当年否定 Hilbert 程序更剧烈：程序员已经开始放弃阅读 AI 生成的代码，即使该代码通过全部测试或形式化验证。

作者的核心主张是：程序与证明在 Church-Howard 对应下等价，因此“AI 生成但人不读”在数学和计算中是同一行为。

Jev 能解析 CSV 吗？

由逗号连接且未加引号的单元格在解析时存在歧义。

针对每个逗号提出一个二元问题，Jev 的准确率达到98%，每300行收费8美分；

而本地75亿参数模型在耗时增加200倍的情况下，准确率为82%。

想想那只变色龙

在《功夫熊猫4》中，变色龙并没有击败阿宝，人工智能也不会击败我们。

Relation Algebra ≠ Relational Algebra

Relation algebra (Tarski's algebra of binary relations, equivalent to three-variable first-order logic) is not Codd's relational algebra, even though Wikipedia and others have conflated them.

It under...

What if SELECT, FROM, WHERE were functions?

Introducing Prela, an embedded query language built on Tarski's Algebra of Relations instead of Codd's: every table decomposes into binary relations over columns, and `SELECT`, `.

and`, `.

eq`, and `WHE...

Value Polymorphism in Rust

Haskell lets a value like `def` mean different things at different types.

Rust doesn't — but generic functions are first-class zero-sized values whose type parameters are filled in by inference, which...

通过继续调用传递数据库

一种用于关系代数的清洁、模块化延续传递风格解释器如何编译为融合列式执行——通过 Julia 的内联功能免费恢复列存储性能。

简单且正确的快照隔离

快照隔离并不能保证可串行化，但通过单行变更——即检查是否为陈旧读取，而非陈旧写入（写入快照隔离）——即可解决这一问题。

教学技巧

我在课堂上常用的一些小技巧：用毛绒玩具来提问，用小测验代替评分作业，将幻灯片用作讲义笔记，通过Pandoc实现Markdown格式的幻灯片，以及对多选题采用汉明距离评分法。

Join Trees, the "Hard" Way

Understanding alpha-acyclicity and join trees for conjunctive queries, and their role in the BCY algorithm.

4 Ways to Improve A Perfect Join Algorithm

Four practical enhancements to Yannakakis's algorithm: Bloom filters, aggregate pushdown, nested representations, and on-the-fly semijoins.

A Perfect Join Algorithm

An introduction to Yannakakis' instance-optimal algorithm for acyclic join queries.

DuckDB Considered Harmful

Why blindly demanding comparisons to state-of-the-art systems like DuckDB is hurting database research.

Method of Four Russians

A detailed explanation of the Four Russians algorithm for boolean matrix multiplication and transitive closure.

Completeness of Equality Saturation

Proving equality saturation is complete for equational proofs via Birkhoff's theorem.

Reading Papers in a Paper-Reading Seminar

An experiment in actually reading papers during class instead of just presenting them.

Duality in Linear Programming

A geometric interpretation of the weak duality theorem.

The Entropic Framework for Cardinality Bounds

Using information theory to estimate join output sizes via entropy and information inequalities.

Relative Safety in Relational Calculus

On deciding whether a relational calculus query has a finite answer on a given database.

How to Check 2 SQL Tables are the Same

Comparing two SQL tables for bag equality is surprisingly tricky.