Tau Language

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.

🔗 Original source & video: Tau Language: The Software Synthesis Future [Sponsored] - Ohad Asor