1982 年，美国哲学家克里普克（Saul Kripke）出了一本小书，讲他从维特根斯坦那里读出来的一个难题。

假设你这辈子算过的加法，数都不大，57 或更大的数从来没加过。现在有人问你：68 加 57 等于几？你说 125。

一个怀疑论者站出来说：你凭什么确定？也许你过去说“加”，意思一直是另一个函数。他管它叫 quus：两个数都小于 57，就照常相加；否则，一律等于 5。照这个意思，答案应该是 5。

翻遍自己的过去，你也找不到反驳他的证据：算过的每一道题，加法和 quus 给的答案都一样；脑子里那句“把两堆东西数到一起”，你也只用过有限次，他照样可以换个方式理解。

这个问题看着像抬杠，哲学家们却为它争了四十多年。（这只是克里普克对维特根斯坦的一种读法，不少维特根斯坦专家并不买账，学界干脆管它叫“克里普克的维特根斯坦”。）它问的是：一个词的意思，到底被什么东西钉死？

哲学家的 quus 是编出来的，计算机里却真有一个。

计算机存整数，用的是固定的位数。Java 的 int 有 32 位，最大能装 2147483647。再加 1，它不报错，也不变成 2147483648，而是绕回最小的负数：负的 2147483648。

这很像汽车的里程表。五位的里程表走到 99999，再走一公里，就回到 00000。只不过计算机的这一圈，一半是正数，一半是负数，最大的正数和最小的负数挨在一起。

它就是一个 quus。在小的数上，它和数学课上的加分毫不差；走过某个界限，答案就变了样。克里普克的界限在 57，Java 的在二十一亿多；克里普克的 quus 答 5，Java 的绕回负数。

这不是 Java 一家的毛病。机器的内存是有限的，任何能被执行的“加”，总有一个走不到的远处，在那里它和数学课上的加分了家。所以我的看法是：每个程序，都偷偷选了一个 quus。

平时谁也走不到那么远，可总有人走到了。

2015 年，美国联邦航空局发了一份适航指令：一架波音 787 如果连续通电 248 天，四台发电机控制器可能同时进入保护模式，整架飞机断掉交流电。指令里写得很直白：控制器内部的一个软件计数器，连续通电 248 天后会溢出。指令没说这个计数器有多少位，但这个天数很好推：如果它每百分之一秒加 1、用 32 位来存，正好在 248 天多一点走到头。

《江南 Style》那次更像个玩笑。2014 年 12 月，它的播放量越过了 2147483647。YouTube 发帖开玩笑说，他们从没想过一段视频的播放次数会超过 32 位整数能装的数，看来得升级了。其实他们几个月前就把计数器换成了 64 位，这次只是借机埋了个彩蛋。连玩笑都选这个数，可见程序员对它有多熟。

真闯了祸的是 Ariane 5。1996 年 6 月 4 日，这枚欧洲火箭首飞。主发动机点火约 37 秒后，也就是离地才 30 秒左右，它突然偏离航向，随即解体自毁。事后调查发现，惯性导航软件要把一个和水平速度有关的数，从 64 位的小数转成 16 位的整数。16 位最大只能装 32767，那个数太大，转换出错。这段软件是从老火箭 Ariane 4 上搬过来的，老火箭飞得慢，从来走不到那个远处。

另一个日子早就写在了日历上。很多老系统从 1970 年 1 月 1 日起，每秒加 1 记时间，用的也是 32 位。到 2038 年 1 月 19 日 3 点 14 分 7 秒（世界协调时），它就走到头了；再过一秒，时间跳回 1901 年。

各种编程语言选的 quus，还不一样。

Java 悄悄绕回。C 的标准干脆说，有符号整数越界是“没有定义的行为”，编译器可以假定它永远不会发生，再据此优化你的代码。Python 的整数一直往上长，直到内存用完。Swift 当场报错停下。Rust 在调试时报错，正式发布的版本默认绕回。JavaScript 的数字其实都是小数，过了 9007199254740991，再加 1 就可能纹丝不动。

有的图快，有的图安全，有的图省事，各有道理。可放在一起看，这是六个不同的“加”。

麻烦在于，写代码的人常常以为自己用的是数学课上的加。2006 年，Java 标准库的主要作者之一 Joshua Bloch 写了一篇博客，标题大意是“几乎所有的二分查找都是坏的”。二分查找要找中点，最自然的写法是把两端加起来除以 2。这行代码在数学课的加里永远对；在 32 位的加里，数组一旦长到十亿多个元素，两端一加就越界，算出一个负的位置。这个错误在 Java 自带的库里待了九年左右。他还指出，Jon Bentley 在经典的《编程珠玑》里写过一段二分查找，还证明了它是对的，结果也有同样的毛病。

说绕圈的加法“错了”，其实冤枉它。它是另一套完完整整的数。

数学家早就认识它：除以 4294967296 取余数的算术。在这套数里，交换律成立，结合律成立，每个数都有一个“相反数”，加起来等于 0。代数里的那些好性质，它几乎全有。

Java 的语言标准还专门写了一句：整数的加法和乘法，可以证明满足结合律；小数的不行。

绕圈的加法只丢了一条：越加越大。在圆圈上，往前走一步，可能走回了起点的另一边。还有一个有点滑稽的后果：最小的那个负数，取相反数还是它自己，所以它的绝对值是负的。Java 的官方文档里专门提醒过这一点。

小数的加，丢得更多。计算机里的小数大多按一个叫 IEEE 754 的标准存，精度有限。先算 0.1 加 0.2，再加 0.3，得到 0.6000000000000001；先算 0.2 加 0.3，再加 0.1，得到 0.6。结合律没了。还有一个叫 NaN 的特殊值，意思是“不是一个数”，它连自己都不等于。

所以与其问哪种加法对，不如问每种加法守住了哪几条定律、丢了哪几条。写程序的人手里，攥着的就是这张表。想把一大堆数分给一千台机器各加一部分、最后再合起来，靠的是结合律；用小数这么干，分法不同，结果就可能差一点点。

还有更怪的：有的定律能运行，有的不能。

自然数的加法，可以只用两句话来定义：任何数加 0，还是它自己；一个数加上“某数的下一个”，等于“它们的和的下一个”。通常认为，最早这样定义加法的是德国数学家格拉斯曼（1861 年）；后来戴德金说清了这种定义为什么站得住，皮亚诺把它写进了公理。

这两句话是定义，也是程序。把它们从左往右当规则用，一步一步就能算出 2 加 3。每一步，把右边的一颗珠子挪到最外层，挪完就停。

交换律不在这两句话里。它是用数学归纳法证出来的定理。证明助手 Lean 里有个很直观的例子：“某数加 0 等于它自己”，系统算一下就认了；反过来，“0 加某数等于它自己”，却得老老实实用归纳法证一遍。你要是把交换律也当成一条规则，从左往右用，2 加 3 变成 3 加 2，3 加 2 又变回 2 加 3，永远停不下来。

计算机科学家很早就撞上了这堵墙。1970 年，高德纳（Donald Knuth）和 Bendix 提出一个算法，想把一组等式自动变成一套“一定会停、答案唯一”的改写规则，相当于把公理编译成程序。交换律这类等式，恰恰是它没法直接处理、必须另想办法的典型。

Lean 里也看得到这条界线。你可以在里面声明一条公理，它只有名字，没有可以执行的内容。一个定义要是靠选择公理这类公理“凭空”拿出一个值，Lean 就要你在它前面标上“不可计算”，它没法被编译成能跑的代码。

公理说的是“世界是这样的”，程序说的是“这样一步一步算”。一条等式能不能运行，要看它能不能只朝一个方向用，而且一定会停。交换律是真的，可它跑不起来。

再回到克里普克。他其实早就想到过计算机。

有人会说：我说的“加”，由我脑子里那台“计算机器”决定。克里普克的回答大意是：真实的机器是有限的，还会出故障；什么叫“出故障”，得看设计者想让它算什么。这样一来，问题又被推回了设计者的意思，怀疑论者照样可以追问。（据斯坦福哲学百科对原书这一段的概述。）

他自己给的出路，是所谓的“怀疑论的解决”：一个词的意思，不是哪个人脑子里的某个事实，而是靠一群人共同的做法维持的。大家都这么用，谁用得不一样，大家会纠正他。

在我看来，编程把这条出路落到了纸面上。一门编程语言的标准，就是一群人把“加”的意思一条一条写下来、吵清楚的协议。Java 的标准规定越界时取结果的低位，C 的标准规定有符号整数越界“没有定义”，连“这里不管”都是写进条文的决定。到了程序这里，“加”的意思不靠哪台机器，也不靠谁的念头，靠的是一份书面约定，每一个输入它都给了说法。

代价是有限：能执行，就得装得下，装得下就有尽头。所以这份约定钉死的，总是某一个 quus。

说到这里，我想给编程下个定义：给一个词有限而确定的意思，并且选定它守哪几条定律。

这个定义能解释不少事。很多 bug，就是你以为某条定律成立，可你选的那个“加”偏偏丢了它，比如那行求中点的代码。好的程序员做两件事：把分岔的地方推到用户永远走不到的远处（64 位的秒计数器，要过两千九百多亿年才走到头），或者让程序走到那里时大声报错，而不是悄悄换一种意思。今天让 AI 帮你写代码，这个问题也省不掉：你说的“加”，是哪个加。

克里普克的怀疑论者问的是人：你凭什么确定，自己一直的意思是加法？

人很难回答，所以哲学家争了四十多年。程序员每天都在替机器回答，而且答得一个字都不含糊。我觉得编程特别的地方也许就在这里：很少有哪种写作，非得把“我的意思”说到底不可。

说到底的代价是，说出来的永远是一个 quus。好在，我们可以挑一个好一点的。

“每个程序，
都偷偷选了一种加法。

In 1982 the American philosopher Saul Kripke published a short book about a puzzle he had drawn out of Wittgenstein.

Suppose that every sum you have done in your life used small numbers: you have never added a number of 57 or more. Now someone asks you: what is 68 plus 57? You say 125.

A sceptic steps forward and says: how can you be sure? Maybe whenever you said “plus” in the past, you meant a different function all along. He calls it quus: if both numbers are less than 57, add them as usual; otherwise, the answer is always 5. On that meaning, the answer should be 5.

Search your whole past and you won't find evidence against him. On every sum you have done, addition and quus give the same answer. And the rule in your head, “count the two piles together”, you have also used only finitely many times; he can read it another way just the same.

The question looks like nitpicking, yet philosophers have argued over it for more than forty years. (This is only Kripke's reading of Wittgenstein, and many Wittgenstein scholars don't buy it; the field simply calls it “Kripkenstein”.) What it asks is this: what, in the end, pins down the meaning of a word?

The philosopher's quus was made up. Inside computers, there is a real one.

Computers store integers in a fixed number of bits. Java's int has 32 bits, and the largest number it can hold is 2147483647. Add 1, and it neither raises an error nor becomes 2147483648; it wraps around to the smallest negative number, negative 2147483648.

It's a lot like a car's odometer. A five-digit odometer reaches 99999, goes one more kilometer, and is back at 00000. The only difference is that the computer's circle is half positive and half negative, so the largest positive number sits right next to the smallest negative one.

It is a quus. On small numbers it agrees exactly with math-class addition; past a certain bound, the answers change. Kripke's bound is 57, Java's is a little over 2.1 billion; Kripke's quus answers 5, Java's wraps around to a negative number.

This isn't just Java's problem. A machine's memory is finite, so any “plus” that can actually be run has some far-off place, out of everyday reach, where it parts ways with math-class addition. So my view is this: every program secretly picks a quus.

Normally nobody gets that far. But someone always does.

In 2015 the FAA issued an airworthiness directive: if a Boeing 787 stayed powered on for 248 days straight, its four generator control units could all go into failsafe mode at once, and the whole airplane would lose AC power. The directive put it plainly: a software counter inside the control units overflows after 248 days of continuous power. It didn't say how many bits the counter has, but the number of days is easy to work out: if it adds 1 every hundredth of a second and is stored in 32 bits, it runs out just over 248 days in.

The “Gangnam Style” case was more of a joke. In December 2014 its view count passed 2147483647. YouTube posted, jokingly, that they had never imagined a video would be watched more times than a 32-bit integer can hold, so it looked like they needed an upgrade. In fact they had switched the counter to 64 bits months before; this was just an Easter egg planted for the occasion. That even a joke reached for this number shows how well programmers know it.

The one that really caused a disaster was Ariane 5. On June 4, 1996, the European rocket made its first flight. About 37 seconds after main engine ignition, only some 30 seconds after liftoff, it suddenly veered off course, then broke up and self-destructed. The inquiry found that the inertial navigation software had to convert a number related to horizontal velocity from a 64-bit floating-point number into a 16-bit integer. The most 16 bits can hold is 32767; the number was too big, and the conversion failed. This software had been carried over from the older Ariane 4, which flew more slowly and never got that far.

Another date has long been marked on the calendar. Many older systems keep time by adding 1 every second since January 1, 1970, also in 32 bits. At 03:14:07 UTC on January 19, 2038, the count runs out; one second later, the time jumps back to 1901.

And different programming languages don't even pick the same quus.

Java quietly wraps around. The C standard flatly says that signed integer overflow is “undefined behavior”: the compiler may assume it never happens and optimize your code on that basis. Python's integers keep growing until memory runs out. Swift stops on the spot with an error. Rust reports an error in debug builds and, by default, wraps around in release builds. JavaScript's numbers are really all floating point; past 9007199254740991, adding 1 may not move a number at all.

Some go for speed, some for safety, some for convenience, and each has its reasons. But put side by side, these are six different versions of “plus”.

The trouble is that people writing code often assume they are using math-class addition. In 2006 Joshua Bloch, one of the main authors of Java's standard library, wrote a blog post titled, in part, “Nearly All Binary Searches and Mergesorts are Broken”. Binary search needs the midpoint, and the most natural way to write it is to add the two ends and divide by 2. Under math-class addition this line is always right; under 32-bit addition, once an array grows past a billion or so elements, adding the two ends overflows and gives a negative position. The bug sat in Java's own library for about nine years. He also pointed out that the binary search Jon Bentley wrote in his classic “Programming Pearls”, and proved correct, had the same flaw.

Calling wrapping addition “wrong” is unfair to it. It is a different number system, complete in every way.

Mathematicians have known it for a long time: the arithmetic of remainders after dividing by 4294967296. In this system commutativity holds, associativity holds, and every number has an “opposite”, the two adding up to 0. It has nearly all the nice properties you know from algebra.

Java's language specification even says so explicitly: integer addition and multiplication are provably associative; floating-point ones are not.

Wrapping addition loses just one law: the more you add, the bigger it gets. On a circle, one step forward can land you on the far side of where you started. There is also a slightly comic consequence: the smallest negative number is its own opposite, so its absolute value is negative. Java's official documentation makes a point of warning about this.

Floating-point addition loses even more. Computers mostly store such numbers under a standard called IEEE 754, with limited precision. Add 0.1 and 0.2 first, then 0.3, and you get 0.6000000000000001; add 0.2 and 0.3 first, then 0.1, and you get 0.6. Associativity is gone. There is also a special value called NaN, meaning “not a number”, which isn't even equal to itself.

So rather than asking which addition is right, ask which laws each one keeps and which it loses. What a programmer holds in hand is exactly this table. If you want to split a huge pile of numbers across a thousand machines, have each add up its share, and then combine the results, you are relying on associativity; do it with floating-point numbers, and a different split can give a slightly different answer.

Stranger still: some laws can be run, and some can't.

Addition of natural numbers can be defined in just two sentences: any number plus 0 is itself; a number plus “the next one after some number” equals “the next one after their sum”. The first to define addition this way is usually said to be the German mathematician Hermann Grassmann (1861); later Richard Dedekind made clear why such a definition holds up, and Giuseppe Peano wrote it into his axioms.

These two sentences are a definition, and also a program. Use them as rules from left to right, and step by step they compute 2 plus 3. Each step moves one bead on the right to the outermost layer; once they have all moved, it stops.

Commutativity is not in those two sentences. It is a theorem, proved by mathematical induction. The proof assistant Lean offers a very telling example: the system accepts “a number plus 0 equals itself” just by computing; the reverse, “0 plus a number equals itself”, has to be proved the honest way, by induction. If you also take commutativity as a rule and use it from left to right, 2 plus 3 becomes 3 plus 2, 3 plus 2 turns back into 2 plus 3, and it never stops.

Computer scientists ran into this wall early. In 1970 Donald Knuth and Peter Bendix proposed an algorithm that tries to turn a set of equations automatically into rewrite rules that “always stop and give a unique answer”: in effect, compiling axioms into a program. Equations like commutativity are the classic case it cannot handle directly; they need some other trick.

You can see the same line in Lean. You can declare an axiom there; it has only a name, with nothing that can be executed. If a definition pulls a value “out of thin air” using an axiom like the axiom of choice, Lean makes you mark it “noncomputable”, and it can't be compiled into code that runs.

An axiom says “the world is like this”; a program says “compute it like this, step by step”. Whether an equation can run depends on whether it can be used in one direction only and is sure to stop. Commutativity is true, but it can't run.

Back to Kripke. He had, in fact, already thought about computers.

Someone might say: what I mean by “plus” is settled by the “calculating machine” in my head. Kripke's reply, roughly: real machines are finite and can break down, and what counts as “breaking down” depends on what the designer meant the machine to compute. So the question is pushed back to the designer's meaning, and the sceptic can press it just the same. (This follows the Stanford Encyclopedia of Philosophy's summary of this passage of the book.)

His own way out is the so-called “sceptical solution”: the meaning of a word is not some fact inside anyone's head, but is kept up by the shared practice of a community. Everyone uses the word the same way, and whoever uses it differently gets corrected by the others.

As I see it, programming puts this way out down on paper. A programming language standard is an agreement in which a group of people write down the meaning of “plus” clause by clause and argue it out. The Java standard says that on overflow you keep the low-order bits of the result; the C standard says that signed integer overflow is “undefined”, so even “not our concern” is a decision written into the text. In a program, the meaning of “plus” rests on no particular machine and on nobody's thoughts, but on a written agreement that has something to say about every input.

The price is finiteness: to run, it has to fit; to fit, it has to end somewhere. So what this agreement pins down is always some quus.

So here is how I would define programming: giving a word a finite, definite meaning, and choosing which laws it keeps.

This definition explains quite a lot. Many bugs are cases where you assumed some law held, but the “plus” you chose happens to have lost it, like that midpoint line. Good programmers have two moves: push the fork out to a far-off place users will never reach (a 64-bit counter of seconds takes more than 290 billion years to run out), or make the program complain loudly when it gets there instead of quietly switching to another meaning. Having AI write your code today doesn't spare you this question either: when you say “plus”, which plus do you mean?

Kripke's sceptic put the question to people: how can you be sure that all along you have meant addition?

People find that hard to answer, which is why philosophers have argued for more than forty years. Programmers answer it for machines every day, and leave not a single word vague. This, I think, may be what makes programming special: few other kinds of writing force you to spell out “what I mean” all the way down.

The price of going all the way down is that what you say always turns out to be a quus. Luckily, we get to pick a better one.

“Every program secretly
picks a kind of addition.