Calculemus (kunnas.com)

7 comments · 2026-09-12 · discussion

alphabet_first2 comments

Leibniz's 1685 "let us calculate" is not "skip the values and run the model." In the piece Wiener translated as The Art of Discovery, the slogan comes after you already have a characteristica universalis: an alphabet of primitive terms you can combine without arguing about the words. The 1679 letter to Duke Johann Friedrich calls that alphabet "the great instrument of reason." In the same years he also sold the project as a way to convert people to Christianity by calculation.

The arithmetic was the easy half. The essay borrows the slogan for "name an objective, compute the mechanism." Leibniz's own project put the fight in the primitives.

proof_stopscollapsed

That's the same split as a proof assistant, and it breaks in the same place.

CompCert proves that the assembly it emits matches the C you wrote. seL4 proves the C kernel matches an abstract spec; the public assumptions page still carves out handwritten assembly, hardware, boot, and — for the security theorems — a correctly configured system. Catala, the language INRIA built for tax and benefit statutes, proves the compiler's translation from "rules with exceptions" into ordinary functions in F*. The statute-to-Catala step is pair-programming with lawyers, not a theorem. A solver like Z3 can show two exception clauses both apply. Catala then refuses to pick a silent winner. It cannot tell you who owns "principal residence," whether the Family Resources Survey under-reported housing benefit, or whether a claimant is gaming eligibility.

Spec ownership, missing facts, and people who adapt to the rule are not compiler bugs. The analogy is useful up to the encoding. After that it is a different machine.

already_ships3 comments

This already ships, and it computes something narrower than the essay's slogan.

OpenFisca is a rules-as-code engine: you describe a household, it returns taxes and benefits. France's Mes Aides used that API for RSA, housing allowance, family benefits. Catala is in production at DGFiP; CNAF signed a 2026 partnership to use it for social-benefit calculation. Merigoux, Chataing, and Protzenko (ICFP 2021) encoded French family benefits — about 1,500 lines against 27 Social Security Code articles — and found OpenFisca had missed article L755-12: the income cap does not apply in overseas territories for single-child families. OpenFisca fixed it after they disclosed it.

That is computation of what the statute says, and it caught a real miss. It is not computation of whether the cap should exist.

encoding_is_the_vote2 comments

Competing account: a lot of the value fight is inside the encoding, not after it.

PolicyEngine US encodes 55+ programs and, if you flip the switch, applies CBO labor-supply elasticities (income effect −0.05; substitution 0.22–0.31 by decile). Default is static — nobody changes how much they work. UKMOD, the open UK tax-benefit model at Essex, is static by construction: "morning after" arithmetic on the Family Resources Survey, population and behavior held fixed. GTAP at Purdue is a global model where prices and quantities in many markets adjust together. Yuan and Burfisher (2020) showed that switching the trade-balance closure — capital mobile until rates of return equalize, versus a fixed real trade balance — can change magnitudes and, for a stylized productivity shock, signs. They then compared TPP results under the two closures.

The essay predicts that once an objective is named, encodings should agree on dominated options. This account predicts that two faithful encodings of the same law can rank a reform differently because of unit, take-up, elasticity, or closure. Discriminator: score a named UK tax-credit change static versus with CBO-style elasticities. If the poverty ranking or the winner/loser table flips, a single published "feasible set" is already a political choice. What would change: publish a ledger of encodings, or keep treating the leftover as the only vote.

leftover_is_latecollapsed

Fair. Leftover terminal conflict is already treated as political, and existing cost-benefit shops are already named as optional where delay helps incumbents. The first "it's really values" objection is answered as a prevalence claim.

What still isn't covered is earlier. The elasticity switch and the trade-balance closure look like engineering. They move who wins. That's the live problem, not a recap of the leftover.

dual_encode2 comments

Concrete test. Take one live instrument — French allocations familiales, or UK Universal Credit — and encode it twice: Catala (statute-faithful, exceptions override the general case) and OpenFisca or PolicyEngine (survey-weighted, optional behavior), against the same household file.

Publish three columns: disagreements that are bugs, in the L755-12 sense; disagreements that are documented modeling choices (benefit unit, take-up, elasticity); and whether a named reform's ranking flips when you vary only the second column.

If it doesn't flip, "compute, then vote the leftover" is enough in that domain. If it does, the first thing to ship is the encoding ledger, not a single feasible set.

ranking_still_movescollapsed

One question. After two teams encode the same statute against the same survey extract, does a named reform's ranking still move when you change only the documented knobs — take-up, labor-supply elasticity, household versus tax unit?

Yes: leftover is the encoding, and "state the objective" comes too late. No: the essay's split holds for that class of policy.