Every MySQL schema that’s been around for a few years collects indexes nobody remembers adding. Some were for a report that was retired. Some came from an ORM migration. A few were added “just in case” and never used. They all cost something: extra writes on every INSERT and UPDATE, increased buffer pool pressure, larger … Continued

The post Multi-Node Unused Index Verification appeared first on Percona.

Earlier this year, we introduced PSMDB Sandbox, a lightweight web UI that sits on top of our Terraform and Ansible automation for MongoDB. Since then, the project has changed a lot. It has a new name and repository, and it supports many more Percona products, MongoDB features and platforms. In this post, I will go … Continued

The post What’s New in PSMDB Sandbox: Six Months of Updates appeared first on Percona.

Welcome back to Village News, our curated roundup of MySQL and database news. This week, plans for FOSDEM 2027 took shape, with a new M-Ecosystem devroom and MySQL Belgian Days opening their calls for papers.

If you want to get these updates, just subscribe to the blog.

Enjoy!

MySQL

We loaded 990,000 OpenAI embeddings of 1,536 dimensions into six databases that index vectors themselves, built an HNSW index in each, and measured five things: time to a queryable index, storage and memory, recall against throughput, throughput under concurrent clients, and what happens when 10% of the corpus is rewritten. Same host, same container shape, … Continued

The post Benchmarking Vector search in six database engines appeared first on Percona.

Back in December I introduced Percona Load Generator for MongoDB Clusters (PLGM), a benchmark tool built around one idea: test your database with your own schema and your own queries, not some random data. At the time, PLGM was a command-line tool. You edited a YAML file, ran the binary, and read the numbers in … Continued

The post PLGM Has Grown Up: A New UI and Many More Features appeared first on Percona.

  Percona Operator for MySQL 1.3.0 is out. This release moves three things forward for teams running MySQL on Kubernetes: the operator now tunes MySQL for you based on the pod resources, async clusters can fail over without losing data in flight, and point-in-time recovery works on clusters where binary logs are encrypted at rest. … Continued

The post Percona Operator for MySQL 1.3.0: autopilot tuning, zero-data-loss async failover, encrypted PITR appeared first on Percona.

This blog post was born of a discussion with a colleague in Percona Support, who also co-authored it with me here on the use of the ARBITER feature in MongoDB installations nowadays. Turns out, after analyzing past real cases we’ve faced in support, maybe it’s time to say goodbye to ARBITERS. We are not saying … Continued

The post Why you should stop using ARBITERS in MongoDB appeared first on Percona.

Probably everyone responsible for managing database servers at some point realizes that it would be helpful to have a tool capable of extracting data directly from raw database files. Something completely offline, without the need to have a running database server, and that would work with data directories, files, or binary backups (storage volume snapshots, … Continued

The post How to Extract Data from InnoDB, MyISAM, and MyRocks Files Without a Running Server appeared first on Percona.

This NeurIPS'26 workshop paper takes TLA+ specs from GitHub, translates them into Verus, and has LLM agents prove the safety and liveness properties in the specs.

The motivation

The paper aims to address two problems it raises with TLA+. First, nothing ties the spec to the code, so they drift apart. And second, it claims that proof support is thin: TLC only checks small configurations, and TLAPS is weak on liveness.

They abandon pursuing the first weakness they raise at the onset of the paper. Closing it needs a proof that the generated Rust code (which it turns out TLA-Verus doesn't produce anyway) refines the spec, so they list this as future work. It gets worse though. There is no refinement proof between the TLA+ spec and the Verus spec either. Nothing establishes that the translated Verus spec means what the original meant. (Trace validation, meanwhile, is a viable way of tying TLA+ to implementation code, and has been getting a lot of attention recently.)

They dedicate the paper to addressing the second weakness, but I think they  understate the TLAPS capability for doing temporal proofs. Writing `BY PTL` on a proof step tells TLAPS to treat that step as propositional temporal logic and send it to LS4, an LTL decision procedure. Coalescing (Doligez, Kriener, Lamport, Libal, Merz) is the technique that abstracts the first-order parts of a TLA+ obligation into propositional atoms LS4 can handle. Lamport's temporal proof rules are all there, including WF1, the rule that turns a weak fairness assumption on an action into a leads-to conclusion. The limitation is that TLAPS reasons poorly about ENABLED, and discharging the enabledness side conditions of WF1 is where a liveness proof needs more work. All this to say, TLAPS has temporal proof capability, and last time I used Claude Code to write TLAPS proofs, I was surprised by how well Opus was able to write TLAPS proofs. I expected the paper to compare against TLAPS proofs, but unfortunately that is missing.

Verus, the Rust verifier, is really cool though. It can host temporal logic. It is auto-active, which is the middle ground between a model checker you push a button on and a proof assistant like Coq or Lean you drive yourself. Here you annotate the program with preconditions, invariants, and lemmas, and an SMT solver discharges the resulting obligations automatically. So instead of writing a proof, your job (or more like your LLM's job) is to figure out which hint the solver is missing. Anvil (OSDI'24) demonstrated this capability by proving liveness of Kubernetes controllers, and it did so by building temporal logic as a Verus library, since Verus itself knows nothing about [] and <>. This paper takes that library almost directly to use `always`, `eventually`, `leads_to`, weak fairness, and pre-proven lemmas like WF1. The game plan of the paper is to move the TLA+ spec into Verus, prove things there leveraging Anvil, and later (in the long term plan) prove that the Rust code written refines the proven Verus `spec`.

Some background on Verus is in order here. A Verus file holds three kinds of code. `spec` code is mathematics: it never runs, and it can use unbounded integers and infinite sets. `proof` code is ghost code, lemmas that exist during verification and are erased afterward. `exec` code is real Rust that compiles and ships, and its preconditions and postconditions are written in terms of the `spec` functions. All three live in one file to keep the specification from drifting away from the implementation.

In this paper there is no `exec` code. Every task is `spec` and `proof` only. The translated TLA+ state machine is a `spec` function relating one state to the next, and what the LLM fills in is an empty `proof fn`. Nothing here compiles to a binary executable code. So the distinguishing feature of Verus from other SMT-backed provers is turned off for the entire corpus. Frankly, I can't see how code generation for a distributed system could be made from `spec` automatically even with LLMs.

The pipeline

OK, I got carried away with the motivation and went into too much detail already. Let's backup and checkout the pipeline. The paper's main contribution is the prover-reviewer loop, which is a way to get LLMs to prove temporal properties of TLA+ specs. The pipeline has three stages: translation, proof search, and merge control.

The unit of work throughout is a (spec, property) pair: that is a whole TLA+ specification together with a single property to prove about it. Each pair becomes its own self-contained Verus file carrying exactly one open proof obligation. (Me thinks this is not a sustainable way to generate code from a real system.) Since a module usually declares several properties, pairs provide an inflated way to count: the 16,459 pairs come from only 2,734 TLA+ modules in 838 GitHub repositories, a median of 5 properties per module. The same specification gets translated and proved over and over, once per property.

Translation comes in two flavors. TranSpec is a deterministic Rust transpiler. It infers types for untyped TLA+, synthesizes termination measures, and places SMT triggers. The other flavor is an LLM translator checked by an LLM judge, without any proof for the translation.

Proof search uses a prover agent and a reviewer agent with fresh context. Verus only says which assertion failed, but gives no counterexample, so the reviewer agent supplies the semantic feedback.

A gatekeeper controls the merges, a signed append-only ledger, and a git hook. Anti-cheat checks reject any net-new `assume`, `admit`, or `external_body`. The prover cannot merge its own work. This prevents the proof agent from reward hacking.

The corpus

The paper runs three separate experiments. The first is the full corpus sweep via the prover-reviewer pipeline, driven by Opus. They tried 16,459 (spec, property) pairs. TranSpec translated 6,070 and 5,160 were well-posed. The prover closed 3,094 of those. Liveness was the weakest type: 304 of 809, about 38%. Proofs cost about $2 each. On the agentic side the losses move to a different stage: 2,851 pairs are judged unprovable by an LLM and dropped, with nothing checking that verdict.

The surviving corpus is lopsided. The paper splits safety into three buckets. "Invariance" is a plain state invariant: []P for a state predicate P. "TypeOK" is the type-correctness invariant, pulled out separately. "Safety" category is reserved for everything that is not a single state predicate. Of the 5,160 well-posed algorithmic tasks, invariance and TypeOK together are 83%, liveness is 809 tasks or 16%, and that last "safety" bucket is 50 tasks, 1%. Safety is scarce because TranSpec is bad at those forms rather than because GitHub lacks them: of the 630 safety properties the agentic pipeline translated, 578 have no usable algorithmic bundle at all.

The benchmark

The third experiment drops the reviewer and the gatekeeper. A model gets the task file and runs Verus, up to 10 attempts. So the prover-reviewer loop, the paper's most interesting contribution, is absent from every number in the model table.

The set is 40 tasks, 10 of each property type, in both encodings, and eleven models at pass@3. Opus-5 and GPT-5.6-sol-pro solve everything; gpt-oss-120b solves nothing. Nine of eleven do worse than on verusbench, DeepSeek-R1 falling from 74.7% to 17.5%. Liveness is again the hardest type: models solved 58 of 110 liveness attempts, against 73 to 78 for each of the other three types.

That 53% on liveness looks better than the 38% from the corpus sweep, but the two are not the same question. The second of seven selection criteria is that the task be "known provable", so the 40 tasks are drawn from the 3,094 the prover already closed. The ten liveness tasks come out of the 304 successes, never the 809 attempts. Which is also why the top of the table saturates: Opus-5 scores 100% on a set filtered by what Opus-5 could prove.

I think the task generator is really the useful thing here. Normally a person has to construct/curate a usable/challenging task, which is why verusbench has only 150 tasks. Here Verus decides it. In TLA-Verus, a translation is kept only if it compiles and verifies with exactly one error, the open proof obligation. Zero errors means the property was already true with an empty proof, so there is nothing to prove (145 such tasks were dropped). Two or more errors mean the translation is broken. That said, this check also has drawbacks. Compiling with one error says the file is well-formed Verus with a proof obligation pending, but it does not guarantee that a proof is possible. The property may be false in the original spec, or the translation may have made it false, and then the prover just burns tokens only to record this task as unproven. The paper admits this type of impossible proof is indistinguishable from a proof that was merely hard. The opposite case is worse still: if the translation breaks the state machine instead of the property, the property holds for free and the proof is easy. That is shown in Appendix C.2: their vacuity filter misses it, because that filter only catches tasks that verify with an empty proof. But this may not be a big problem, because these specs come from GitHub and most were model-checked by their authors before being committed, so the properties would be "mostly" true.

Goodhart’s law, that any measurable target stops being useful when people start optimizing for it, very much holds in database benchmarking. That is not new, of course. Famously, TPC-D got retired when people optimized so much for it that the query runtimes converged towards zero due to excessive caching. TPC-H fixed that by declaring itself to be an ad-hoc benchmark, and explicitly forbidding things like exploiting knowledge about the workload or caching results (and a number of other optimizations).

We now see the same problem with the ClickBench benchmark, heavily accelerated by today’s use of AI code generation. If you tell an AI to make the queries faster, it will make the queries faster, regardless of whether this is a generally plausible approach or not. For example, the pgrust implementation performs group-by aggregations on string columns purely on the hash value, ignoring the long string content. That is a great performance boost, of course, and works for this benchmark, but can produce wrong results. Is it faster? Yes. Is it a plausible optimization? Probably not. And it does many other things: For example, ClickBench repeats certain predicates across queries, and thus pgrust caches the predicate, completely eliminating the query cost the second time. Or for query Q17, which returns tuples grouped by userid, it makes use of the fact that a) tuples are roughly clustered by userid, and b) the query specifies a limit clause without order by. Thus any userid will do, and it never reads most of the data. A human would not do these tiny micro-optimizations, because they are unlikely to be relevant in general use cases, but an AI can of course look at each query in detail and tune for it.

Part of the problem is, of course, ClickBench itself. The benchmark is not well specified in what is permitted and what is not, there is no update stream, the queries are very simple, share predicates, are underspecified, etc. But the fundamental problem is independent of that concrete benchmark: The moment we start aggressively optimizing for a specific benchmark, the benchmark stops being very useful. Historically, that pressure was reduced a bit by the requirement that systems be generally useful. That is, they did not just want to perform well in benchmarks but also to be useful for their customers. That is, of course, not a concern for vibe-coded execution engines.

It is not clear what to do about it. Our SQLStorm proposal tried to address this by having tens of thousands of queries, which makes overfitting harder. No human would fine-tune their system to such a huge workload. But with AI tools we could even investigate ten thousand queries in detail if needed, so that is not a real defense.

I think that to be meaningful, a benchmark has to a) like TPC-H, be ad-hoc, and forbid exploiting prior knowledge and any form of intermediate result caching. If we don’t do that, execution times converge towards zero. And b) the benchmark has to include some form of update stream, as otherwise overly aggressive read-only or read-mostly systems will always outperform systems that offer full transactional support. And c) the benchmark has to be truly ad-hoc, in the sense that the systems tested have to be older than the benchmark. One way to fight Goodhart’s law would be to (automatically) come up with a new benchmark from time to time, and then measure the systems that existed before the benchmark. The caching/pre-computation problem still remains, of course, but at least that would prevent the over-aggressive adjustment to just one specific benchmark.

Interestingly, the machine learning community has struggled with exactly the same problem for years, and we should probably borrow some of their ideas. Kaggle competitions, for example, rank submissions on a hidden test set that participants never see, which makes overfitting on the public data pointless. Similarly, benchmarks like LiveBench regularly release new questions to make sure that models cannot have seen them during training. For database benchmarking that could mean keeping the actual benchmark queries secret and only publishing a representative sample for development, or, even better, generating a fresh workload for every evaluation round. SQLStorm already uses generated queries, so producing a new query set from time to time would be fairly easy. We would probably want a more generic approach (higher variety in schemas, update streams, transactions, etc.), but that seems to be a direction that would help keep benchmarks meaningful.

I have come to suspect that to most people thinking is painful. Some of us are addicted to thinking. Some of us find it a necessity. Johnny enjoyed it. I even have the suspicion that he enjoyed almost nothing else.

-- Edward Teller, eulogizing John von Neumann

I listened to Ananyo Bhattacharya's "The Man from the Future: The Visionary Life of John von Neumann" in my car during the many commute hours Bay Area traffic afforded me. I thought I should share the Johnny phenomena here.

I knew about von Neumann being a very influential mathematician/scientist/engineer but the full list still left me bedazzled. In his 53 years of life (1903-1957), von Neumann seeded so many fields. Every time there was an important discovery in physics, mathematics or computation, John von Neumann was there. Set theory and the foundations of mathematics. The mathematical formulation of quantum mechanics. Operator algebras (still called von Neumann algebras). Ergodic theory. Game theory. Expected utility theory (which is the foundation of most of modern mathematical economics). The Monte Carlo method. The stored-program computer architecture that every machine you have ever touched is built on. Numerical weather prediction. Fault-tolerant computing. Self-reproducing automata (cellular automata), and arguably, the logical structure of molecular biology, four years before Watson and Crick. There is also, unfortunately, the implosion lens for the Nagasaki bomb, and a decade of hawkish nuclear strategy.

Early years

At six, Janos (the OG hungarian name for Johnny) could divide eight-digit numbers in his head and hold a conversation in ancient Greek. He later added Latin, French, German, English, and Yiddish.  The rumor was that he remembered everything he ever read. Many years later Herman Goldstine decided to test this by asking him to recite "A Tale of Two Cities." Von Neumann started on chapter one and had to be asked to stop fifteen minutes later.

Budapest around 1900 produced an absurd cluster of minds: von Neumann, Eugene Wigner, Edward Teller, Leo Szilard, Paul Erdős, Theodore von Kármán, George Pólya. When several of them turned up at Los Alamos and realized they had gone to high school together, Szilard joked that Hungary was a cover story for a Martian landing. But even inside the Martian cluster, von Neumann was the outlier. Wigner, a Nobel laureate himself, was asked at Los Alamos to explain the Hungarian phenomenon and said there is only one phenomenon that is worthy of explanation, and that phenomenon is John von Neumann. The cluster may be less mysterious than it looks: Budapest was one of the few genuinely welcoming places in Europe for Jewish families, and it pushed them toward the professions the nobility considered beneath them, mathematics among them. The schools then did the rest, with a nationwide math competition and top quality high school teachers.

From the pedagogical perspective, two things stood out to me from Johnny's early years. The first is the dinner table. Von Neumann's father Miksa (Max), a lawyer turned banker so successful that the Emperor ennobled him for service to the national economy, ran the evening meal as a seminar. He would start by going through his own day: the cases he argued, the deals he negotiated, whatever was on his mind. Then each of the three boys would present on what they had been reading. The whole family would then argue about Heine's poetry, or antisemitism in Europe, or the paradoxes of omnipotence. Sometimes Max would bring home business clients, and the boys were allowed to grill them about whatever they wanted funded. Frequent guests included the director of Budapest's Theoretical Physics Institute and one of Freud's students.

The second is the languages. Max knew the good times could end, told his sons so explicitly, and wanted them able to survive anywhere in any language. He was preparing them to flee. He was right. When John was fifteen, the communists took over Hungary and targeted rich families like his. A few months later the counterrevolutionaries beat the communists and then massacred thousands of Jews for supposedly collaborating. The von Neumanns survived by leaving the country at the right moments, and possibly by being too rich.

Johnny's first ten years included no formal schooling at all, because organized primary schools were not a tradition there yet. He had governesses, private teachers, and his father's enormous library, and he apparently used it to memorize a 44-volume German history of the world, which he would later deploy to freak people out at parties.

When he did get to the Fasori Gymnasium at eleven, the math teacher, László Rátz, concluded fairly quickly that he could not teach this kid and arranged a private tutor. The tutor was Gábor Szegő, who went on to chair the math department at Stanford. Szegő is said to have come away from the first lessons in tears at what the boy could already do. The results of this tutelage showed up a couple years later. At seventeen Johnny gave a new definition of the ordinal numbers, where each number simply is the set of all the numbers before it. Zero is the empty set. One is the set containing zero. Two is the set containing zero and one. And so on up into the infinite ordinals, with nothing but the empty set and a pair of braces to build from. If you think about it, this is a very computer-science-y way to define numbers: an inductive datatype with one constructor. 

He pushed this further in his doctoral thesis a few years later. Set theory at the time was still suffering from the paradoxes, Russell's set of all sets that do not contain themselves being the famous one. Johnny's fix was essentially a type system for sets: the ordinary ones you can put inside other sets, and the oversized ones you can talk about but never use as an element. The paradox then becomes a type error. Note that it is the same abstraction move in both times: take an object everyone thinks they understand, and replace it with the smallest thing that behaves the same way.

Johnny kept doing the same thing in field after field for the next thirty years: arrive, find the smallest set of objects and axioms the mess is actually about, write them down so that everyone can finally argue about the right thing, and then leave before the theorems fell out. Teller said Johnny enjoyed thinking, but I think the addiction was much more specialized than that. His real superpower was "the art of abstraction".

Look at the list from the introduction again with this in mind. Matrix mechanics and wave mechanics looked like rival theories until he noticed they were two coordinate systems on the same Hilbert space. Economists thought comparing preferences across people was hopeless until he asked what minimal consistency axioms a chooser has to satisfy, and derived a cardinal utility scale from them in an afternoon. Self-reproduction looked like it needed an infinite recursion of blueprints until he separated "read the tape as instructions" from "copy the tape as data."

Making quantum mechanics rigorous

Having finished his PhD at 21, Johnny arrived at Göttingen at 22 because it was the world capital of mathematics, under Hilbert. The timing couldn't have been better. Heisenberg, one year older, was down the hall having just invented matrix mechanics. A year later Schrödinger produced wave mechanics in Vienna. The two gave the same answers and implied completely different pictures of reality, and physicists were uneasy with both: matrices were unfamiliar mathematics then, and nobody could say what the waves were. Von Neumann's first move was to prove the two were the same theory in different forms. Then he wrote "Mathematical Foundations of Quantum Mechanics" (1932), which set the whole thing up rigorously in Hilbert space. The author of the book Bhattacharya, who did physics as an undergrad, points out that this is still the most watertight formulation we have. 

Once the math was clean, the measurement problem became more visible. Where does the wave function actually collapse? At the apparatus, the detector, the retina, or the conscious observer? Von Neumann declined to take a position, but proved it does not matter mathematically where you draw the line because the answer comes out the same. That line is now called the von Neumann cut.

Game theory and economics

Nothing much came of game theory until von Neumann proved the minimax theorem in 1928, in his early twenties. Every two-player zero-sum game has a solution: either a strategy one player can pursue to win, or a mixed strategy with randomness in it (e.g., rock-paper-scissors). Then he lost interest and wandered off, as was his habit.

He came back when Oskar Morgenstern turned up at Princeton. Morgenstern, an economist, was stuck on what is essentially a liveness bug in economic modeling: you intervene in an economy, people adjust their behavior in response, which invalidates the model you used to design the intervention, so you build a new model, which they also adjust to. An infinite loop. Morgenstern had concluded that all attempts to model economies must fail, which made him unpopular right up until the Wall Street crash made him look prescient. Von Neumann had the tools to attack the problem. Over about eighteen months they produced the 600-page "Theory of Games and Economic Behavior" (1944) and founded the field. Johnny did this as a hobby. During those same years he was designing implosion lenses at Los Alamos and building the first programmable computers. He would drop in on Morgenstern for a long session and then vanish back into the rest of his life.

Two things from this work are still everywhere. The first is the axiomatization of expected utility. Putting human preferences on a cardinal scale and comparing them across people was considered more or less impossible, and von Neumann sat down one afternoon and did it. This relates uncomfortably with the longtermism material from the Cal Newport/Émile Torres conversation I wrote up recently. Expected value math is a hell of a drug.

The second is its limited model. His framework is built on zero-sum games and on coalitions: given n players, which coalitions are stable? Most of the book is about that. And most of the world is not zero-sum. Nash's non-cooperative equilibrium, which generalizes minimax, is what opened that up, and von Neumann rejected it essentially out of hand when Nash walked into his office. To him it was a trivial step, a fixed-point argument he could see through instantly. He misjudged the importance of the non-cooperative approach. Bhattacharya flags a nice irony here: von Neumann, the alleged Cold War hawk and the model for Dr. Strangelove, built a theory centered on people talking to each other and forming working coalitions. It was Nash, who had trouble with people, who formalized everyone optimizing alone. All models are wrong, but some are useful.

The computer

In 1944 Johnny ran into Herman Goldstine on a train platform at Aberdeen, found out about the ENIAC, and attached himself to the project. In 1945 he wrote the "First Draft of a Report on the EDVAC", laying out the stored-program architecture: one memory holding both instructions and data, a control unit, an arithmetic unit, I/O. That is now the architecture of virtually all computers, from the desktops to smartphones, eighty years later.

Von Neumann was adamant that the technical details go into the public domain, and circulating that draft is exactly what made the architecture unpatentable. So Johnny was also an early proponent of Open Source. He did the same with the IAS machine design, which got copied worldwide and produced a run of machines with goofy names: MANIAC at Los Alamos, JOHNNIAC at RAND, ILLIAC at Illinois, SILLIAC in Sydney, WEIZAC in Israel. For a man who gets painted as the cold rationalist hawk, putting the foundational design of the computing industry into the commons on purpose is a generous act.

He also, with Ulam, invented the Monte Carlo method, then needed random numbers for it and had to invent pseudorandom generation. And he put the first serious application on these machines himself. The IAS Meteorology Project ran the first computerized weather forecast in 1950. Numerical weather prediction, and by extension climate modeling, is a von Neumann production.

Reliable organisms from unreliable components

In 1952 von Neumann gave a lecture series at Caltech titled "Probabilistic Logics and the Synthesis of Reliable Organisms from Unreliable Components." The vacuum tubes of the day failed constantly, and the standard engineering response was to make better tubes. His response was to ask whether you could build an arbitrarily reliable machine out of components that are guaranteed to fail, using redundancy and majority voting, and then to work out how much redundancy you actually need. That is one of the founding ideas of fault-tolerant computing, and gives rise to replicated state machine, quorums, and Paxos.

Self-reproducing automata

In the late 1940s, Johnny started asking what it would take for a machine to build a copy of itself. The naive worry is infinite recursion: the machine needs a blueprint of itself, and that blueprint must include a blueprint of the blueprint, and so on down forever. His solution (worked out with Ulam's suggestion to set it in a discrete cellular framework) was to split the role of the description. You have a universal constructor plus a tape describing it. The constructor reads the tape as "instructions" and builds the described machine. Then it copies the tape as uninterpreted "data" and attaches the copy to the offspring. One description is used twice in two completely different modes. This is the stored-program idea again, three years after EDVAC: the same bits are instructions when you execute them and data when you copy them.

He published this in 1948 and 1949. Watson and Crick published the structure of DNA in 1953. So von Neumann derived, from pure logic, the necessary architecture of biological reproduction. That there must be a stored description. That it must be read in two distinct ways. That this separation is precisely what makes open-ended evolution possible. Translation and transcription. Genotype and phenotype. He got the shape of the answer years before anyone knew what the molecule was.

The 29-state cellular automaton he built to prove it was also, incidentally, the first cellular automaton. Conway's Game of Life, Wolfram's entire research program, artificial life, and a foundations of what people now call synthetic biology all descend from his formal model. "Theory of Self-Reproducing Automata" was published posthumously in 1966.

His last work, also published posthumously, was "The Computer and the Brain" (1958). In it he observes that the brain achieves what it does with terrible arithmetic precision and enormous parallelism, which is the opposite of the machines he had just finished building. There he argues that whatever language the nervous system computes in, it is not mathematics as we understand mathematics. We are still working on this last one!

Personality

Johnny loved parties, loud music, and fast cars. He drove crowded roads like a maniac, and got bored and slowed down on open ones. He wrecked a car roughly every year, usually a Cadillac, "because no one would sell me a tank". An intersection in Princeton was christened Von Neumann Corner for the number of accidents he had there. One of his accident reports says: "I was proceeding down the road. The trees on the right were passing me in orderly fashion at 60 miles an hour. Suddenly one of them stepped in my path. Boom!"

He also did his best work in chaos, and played German march music at volume in his office at Princeton, generating complaints from neighbors who included Albert Einstein.

His detractors called him cold, calculating, and ruthless. He did not join the Manhattan Project colleagues who agonized afterward, and instead he pushed the government toward bigger hydrogen bombs. He advocated an immediate preemptive nuclear strike on the USSR: "If you say why not bomb them tomorrow, I say why not today? If you say today at five o'clock, I say why not one o'clock?" Very brutal. And he said it in public, more than once, to journalists, while sitting on the Atomic Energy Commission. But notice that, this is rooted in his abstraction habit. Model the Cold War as a two-player zero-sum game, assume the Soviets get the bomb soon and would use it, and minimax says strike first. The math checks out, but the problem is the very simplistic model he uses. Stanislaw Ulam, who worked beside him for twenty years, put it as kindly as it can be put: "There was perhaps an inclination to take a too exclusively rational point of view about the cases of historical events."

Paradoxically, the same man was remarkably generous with people. He moved heaven and earth for those he thought were promising: Turing and Mandelbrot both benefited, and he mentored David Blackwell, a Black statistician Princeton did not want, and pushed until they took him. Blackwell wrote later about how much it mattered. Johnny put his own reputation on the line testifying for Oppenheimer, whose politics he did not share. A friend described him as "always gentle, always kind, always penetrating and always magnificently lucid." Teller said: "Von Neumann would carry on a conversation with my 3-year-old son, and the two of them would talk as equals, and I sometimes wondered if he used the same principle when he talked to the rest of us."

Which brings me back to the Teller line I opened with: Johnny enjoyed thinking, and Teller suspected he enjoyed almost nothing else. That is a lovely thing to say about a man at his funeral. It is also the setup for the cruelest possible ending, and Teller knew it when he said it. The cancer, probably from the radiation he absorbed standing around at weapons tests, started in the bone and went to the brain. He had spent fifty years as the fastest mind in any room he entered, and he had to watch that go. Teller: "When [Johnny] was dying of cancer, his brain was affected. I think that he suffered from this loss more than I have seen any human to suffer in any other circumstance".

Johnny remained a game theorist to the end. After a lifetime of culturally Jewish atheism, he asked to be baptized. His daughter attributed it to Pascal's Wager: a small probability of a much better afterlife, against a trivial cost. 

Can we survive technology?

In 1955 von Neumann wrote an essay called "Can We Survive Technology?" He spends most of it on nuclear war, but he touches on global warming. In 1955! And a few years earlier, in a conversation Ulam recalled in his obituary, he had already coined "singularity" (yes, that singularity) for a point where technological progress accelerates past the possibility of predicting what comes next.

This is what he actually argues about whether you can solve this by banning the dangerous technology:

In looking for a solution, it is well to exclude one pseudosolution at the start. The crisis will not be resolved by inhibiting this or that apparently particularly obnoxious form of technology. For one thing, the parts of technology, as well as of the underlying sciences, are so intertwined that in the long run nothing less than a total elimination of all technological progress would suffice for inhibition.

He goes on to say that a ban would have to be worldwide to work, and prohibition of invention runs against the entire ethos of the industrial age, and is not going to be heeded anyways.

So what does he offer instead?

What safeguard remains? Apparently only day-to-day — or perhaps year-to-year — opportunistic measures, a long sequence of small, correct decisions. [...] For progress there is no cure. Any attempt to find automatically safe channels for the present explosive variety of progress must lead to frustration. The only safety possible is relative, and it lies in an intelligent exercise of day-to-day judgment.

And then he names the qualities required: "patience, flexibility, intelligence". So, here is von Neumann, the master of abstraction, with no abstraction to offer. Maybe through his bout of applying minimax reasoning to nuclear strategy, he learned what a formal model is worth when the assumptions are shaky and the stakes are civilizational.