Summary

Asor argues that machine learning remains probabilistic and eventually hits a difficulty threshold, making it unsuitable for software that must never violate a rule. He calls ML a “mathematical miracle” but stresses its PAC ceiling: error never becomes zero and certainty never becomes one. For sufficiently large SAT problems—“hundreds of variables,” in his example—he says even o3, o30, or o300 would become a “coin toss,” while dedicated SAT solvers can handle thousands of variables.
Tau’s proposition is synthesis rather than ordinary verification: users state requirements, and the system generates software guaranteed to satisfy them when the specification is satisfiable. Instead of writing banking code and auditing every balance update, the user states “balance greater than or equal to zero.” Asor’s shorthand is: “You write only the test,” and the computer produces something that passes it across all possible inputs.
The enabling technical bet is that practical logical reasoning has outrun the pessimism behind the 1970s AI winter. NP-complete problems were believed intractable even at modest scale, yet DPLL/CDCL-based SAT solvers and “a bunch of quite trivial heuristics” proved unexpectedly effective. Asor sees an empirical “almost Moore’s law of SAT solvers,” making now the right time to reinvest in logical AI.
Tau’s claimed differentiator is a language that can refer to its own sentences through Boolean-algebra abstraction, while avoiding the unrestricted truth predicate addressed by Tarski’s theorem. Asor abstracts sentences into Boolean-algebra elements, retaining operations such as and, or, not, and semantic equality while discarding internal structure. Adding time plus explicit inputs and outputs lets Tau check whether, for every input, an output exists that meets the specification, and synthesize a program when that condition holds.
Pointwise revision is intended to keep synthesized software editable without rebuilding everything. Tau prefers outputs satisfying both old and new specifications; when none exist, it chooses one satisfying the new specification. That gives users local control while preserving the rest, although Asor concedes that normalization can produce alien-looking specifications and that performance, readability, and explainability remain ongoing efforts.
Blockchain is Tau’s flagship application because the same language can specify contracts, transactions, governance, and changes to governance itself. Asor calls Tau “the end game of all blockchains”: a user could post a knowledge bounty, define acceptable deals, or tell an “automatic businessman” to “make profit for me”—“whenever possible.” The deeper bet is user-controlled software whose governance rules and “laws of changing the laws” are themselves mutable.
Execution risk remains material despite the breadth of the vision. Asor says he finalized the full synthesis algorithm about a month before the interview, but also says the implemented system is currently an interpreter and that synthesis has not yet been implemented. He offers no launch date after being “too optimistic in the past.” AGRS currently exists as a temporary Ethereum token intended to swap into the eventual native token, with a restartable testnet planned before mainnet.

Deep dive

1. Statistical accuracy never becomes a correctness guarantee

Asor starts with admiration rather than dismissal: machine learning can generalize from examples it never saw, which he calls a “mathematical miracle.” But PAC learning promises only “probably approximately correct”; neither zero error nor probability-one correctness is available.
His harder claim is that accuracy improves only up to a problem-complexity threshold. Beyond that, he says a model can become random, particularly on structured logical problems where every constraint must be respected simultaneously.
The concrete specimen is Boolean satisfiability: party-attendance rules such as “if A comes and B does not, C comes.” SAT solvers handle thousands of variables, while Asor predicts that from hundreds of variables even o3, o30, or o300 would offer no more than a “coin toss.”
Polynomial interpolation supplies the analogy: fit 1,000 arbitrary points with a degree-1,000 polynomial and the next point remains unpredictable. An unrestricted concept class has infinite VC dimension; perfect fitting becomes overfitting, not evidence of generalization.

2. Tim’s transduction challenge exposes the actual trade-off

Tim pushes back with improvements in the o-series models and recent work on François Chollet’s ARC challenge using transduction: put test-instance information inside the prediction function and embrace situated complexity rather than relying only on an inductive model trained to generalize to unseen examples.
Asor’s answer is that changing the route to a prediction function does not remove its computational limits. If the class contains arbitrary polynomials capable of fitting everything, interpolation over arbitrary data still has no predictive power.
A smaller class may fail to fit the training data; if it does fit, Asor says there is more confidence—not a guarantee—that it will perform well out of sample.
Tim names the three-way bind—the optimization, statistical, and approximation curses—before asking what logic sacrifices. Asor’s concise answer: “The information has to be there.” Logic works when the requirement can be stated; machine learning remains valuable when examples are all that exist.

3. Logic is for definable rules, while machine learning helps where rules cannot be stated

Face recognition is Asor’s canonical ML case: people recognize a face immediately but cannot adequately put the recognition rule into words. Where a definition is unavailable, examples and a less accurate statistical system may still be “better than nothing.”
Where rules are expressible, he sees indirect encoding through linear algebra as needless. Machine learning can still appear inside a larger logical system: describe the algorithm logically, then combine its guessing component with deterministic requirements governing the rest of the software.
Beneath that engineering split sits a philosophical one: “The finger pointing to the Moon is not the Moon.” Language can point toward physical reality but never touch it; nevertheless, humans live heavily in concepts and communicate with computers through language, so symbolic expression is the natural interface for systems serving human goals.

4. Synthesis replaces implementation with statements about behavior

Asor calls verification “old news.” Verification starts with a system and checks propositions about it; synthesis supplies only the propositions or requirements and automatically generates a system meeting them.
The programming analogy is to write tests without the application. Instead of manually implementing code and then checking it, “write only the test,” after which the computer synthesizes a program that makes that test pass.
A phone that must never transmit a password illustrates universal guarantees: conceptually quantify over all possible inputs and configurations. Asor explicitly says this test cannot be implemented in the literal way described, but says that suitable mathematical frameworks can prove properties over infinite domains and provide guarantees.
Tim objects that passwords could be encoded in infinitely many unforeseen ways. Asor agrees that this could happen, says the password is only an example, and reiterates that the point is to state properties over all relevant system configurations and inputs using a specific mathematical framework.

5. Critical software reveals why requirements matter

For banking software, Asor asks whether anyone would entrust an entire bank to an o3 model; he says even ardent LLM proponents would not. Traditional programmers instead inspect every explicit and implicit balance mutation, still risking omissions.
In Tau, the intended alternative is to state “balance greater than or equal to zero.” An earlier bank rule included an authorization exception, but the Zurich-banker thought experiment moves the discussion from writing software to changing its specification.
The synthesized implementation may vary, but any conforming implementation must respect the formal condition. Asor says Tau’s synthesis framework is intended to handle such specification updates rather than assuming the first formalization remains permanently sufficient.

6. Definability—not a model of the whole world—draws the boundary

Tim invokes the 1980s expert-system bottleneck: rules accumulated special cases until brittle ontologies became unmanageable. Asor rejects the premise that Tau should describe reality comprehensively: “I have no intention to describe the whole real world”; it should capture only what computers must do for human goals.
He separates three limits. Formal languages have only countably many finite sentences, so most mathematical structures are undefinable. Computability theory excludes problems such as the halting problem; computable numbers are countable, while almost all real numbers are uncomputable. Physical reality is stricter still because even “physically exists” cannot be precisely defined.
Asor explicitly distinguishes the computer world, which he says he knows how to treat, from the human and physical worlds, which he says are beyond him.
Programming languages can express anything a computer can do only when the desired behavior is known. If “racist statement” cannot be defined, no formal guarantee can be stated for its detection; users can instead provide examples and accept a less accurate probabilistic system.

7. SAT solvers changed the practical case for logical AI

Asor traces the 1970s logical-AI winter to the Lighthill debate and the belief that NP-complete reasoning was unusable even at small scale. That belief had no theoretical proof, and he says large SAT instances have since provided empirical evidence that the pessimism was misplaced.
The breakthrough is less glamorous than the outcome: DPLL combined with CDCL and “a bunch of quite trivial heuristics” that unexpectedly work. Asor says nobody fully knows why they perform so well, but solver capability continues improving like an “almost Moore’s law of SAT solvers.”
Tim compares this reversal with deep learning’s revival after GPUs, data, and algorithmic changes. Asor draws the investment conclusion explicitly: logical AI was abandoned for presumed computational difficulty, not lack of promise, and practical evidence now justifies renewed building and research.

8. Boolean abstraction gives Tau restricted self-reference

Asor says that a language capable of referring to sentences in the same language is essential for safe AI. Conventional logical AI and logical frameworks also lack this capability without the relevant additional component. He claims to be the only person to have discovered this particular solution.
Tarski’s obstacle arises, in the setting Asor describes, when arithmetic gains a truth predicate taking a sentence’s Gödel number and declaring it true or false. Merely assuming such a predicate within the language permits contradiction, making every statement and its negation provable.
Tau avoids carrying a sentence’s full structure into self-reference. It treats sentences only as Boolean-algebra elements supporting and, or, not, and semantic equality—analogous to sets with union, intersection, complement, and equality but no membership inspection.
Asor’s key restriction is that Tau is its own metalanguage only through this Boolean interface. “We forget about the structure of the sentence,” retaining an abstraction he says is sufficient for practical self-reference without recreating the unrestricted truth predicate.

9. Time, inputs, and outputs turn the algebra into software

Tau extends standard Boolean-algebra theory by permitting references to any algebra element, not only zero and one, and by making its underlying algebra the collection of Tau’s own sentences.
It then adds time—allowing a statement now to be compared with five steps earlier—and distinguishes inputs from outputs. Those additions are what convert a logical language into a software-specification language.
Tim initially describes Tau as guaranteeing a matching output for every input; Asor corrects him. Tau first checks satisfiability: at each time, for all inputs there must exist an output meeting the specification. Only if that property holds can it synthesize a conforming program over the infinite domain of Tau sentences.

10. Infinite implementation space is manageable, but efficiency is unresolved

Synthesis does not enumerate every program; the space is infinite. Asor compares it with proving that a nonconstant complex polynomial has a zero, or choosing a number above 10: mathematics can establish existence and construct an example without scanning an infinite domain.
Tau began with an interpreter capable of executing a specification. Asor says the full synthesis algorithm was finalized about a month before the interview, but also says the currently implemented system is an interpreter and that synthesis has not yet been implemented. The intended output language is C++, although any Turing-complete target could work in principle.
A specification normally admits infinitely many programs. If the backend’s arbitrary choice is unacceptable, the user must add constraints. Later behavior can reveal either a missing requirement or a world that has changed.
Efficiency is a “big difficulty.” The plan is to recognize easy cases, solve logic ahead of time, and emit straightforward input-output functions; SAT or SMT solvers might help, but Asor is unsure. Worst-case program complexity grows as specification size grows, while optimization, readability, and explainability remain ongoing efforts.

11. Pointwise revision preserves old behavior wherever possible

General belief revision is unsolvable: given A→C, B→C, and new information ¬C, one might delete either implication or infer ¬A or ¬B, with no universally optimal choice.
Software outputs create a narrower objective. Tau chooses an output satisfying both old and new specifications when one exists; otherwise it chooses one satisfying the new specification alone. Users state only the change, while the rest remains intact.
Asor calls pointwise revision an answer that “looks very easy” once seen. Quantifier elimination in atomless Boolean algebra can remove existential clauses, and normalization can collapse redundancies, sometimes turning a large specification into one line.
Tim worries that optimization scrubs the developer’s mental provenance. Asor concedes normalized specifications may become less intelligible: interpreters and compilers rewrite code internally, but Tau’s rewritten form is only sometimes better, and no mathematical definition of intelligibility supplies a magic remedy.

12. User control culminates in mutable governance and programmable money

Tau was designed for “1 and only 1 goal”: software controlled by its users. Asor’s categorical pitch is, “I am the user; I am the boss of my computer.” For genuinely user-controlled software, he says there is “no other choice” but to use T technology.
Collective control extends to “laws of changing the laws.” It need not mean equal influence—users might delegate their voice to trusted experts, producing a meritocracy—and the governance mechanism can itself be amended or made resistant to future amendment.
“Tau is a discussion about Tau”: an opinion map records the opinions in a discussion, including which opinions contradict one another; the discussion’s consensus becomes a software update, and even the definition of consensus remains configurable. Asor admits trajectories can deadlock or become sclerotic; logical guarantees and economic incentives mitigate rather than eliminate that risk.
The host frames blockchain as needing Tau; Asor agrees that blockchain needs Tau to be redefined over time by its users. Tau is the flagship special case: its language could define the blockchain, its contracts, and the rules for changing them. Existing smart-contract languages are programming languages, whereas Tau is intended to specify the behavior of the blockchain and contracts at the same level.
The proposed applications include knowledge bounties and an “automatic businessman” given assets, desired outcomes, and acceptable deals. The user can say “make profit for me,” with Asor’s essential hedge—“whenever possible”—and the system is intended to produce the applicable behavior.
Product readiness trails the thesis. AGRS is currently a temporary Ethereum token intended for a future swap; Asor offers no launch date, expects users to discourage forks, and plans a fake-coin testnet that can be restarted after governance deadlocks before rules migrate to mainnet.
His broader economic case is automation: taxes, accounting, transfers, and financial workflows could be programmable rather than trapped in the paperwork and manual processes of 2025. Asked whether manual checks prevent fraud, he does not claim to know; his narrower prescription is to fight “illogicalism” wherever it appears.

Haivivi’s Li Yong on Building a Mass-Market AI Jellycat China's Tech Tightrope: Power, Regulation, and the AI Race with Angela Zhang