Tau Language
Tau synthesizes software from formal specifications: instead of machine instructions, simply say what conditions must hold.
Illustrative: the outgoing amount never exceeds 2,000.
Tau Language overview
A declarative, decidable, and executable formal language. You write sentences that must hold over time. Tau synthesizes correct-by-construction programs from realizable specifications. Programs can reason over one another, this is unique to Tau.
LTL+Past modulo the first-order theory of atomless Boolean algebras. Specifications are elements of such an algebra, so the language can quantify over and refer to them, therefore it is the only language that can reason over its own sentences.
next, finally, globally, until, release, yesterday, once, historically and since
Development with Tau Language
Development is like writing the tests a program must pass, and automatically getting the program that passes them.
Know before you run
Know if a spec will hold before you run it. Tau checks that valid outputs exist for every input sequence, so failures surface at design time rather than in production.
Get a program from the spec
You only write the specification. Tau synthesizes a correct-by-construction program that realizes it.
Updates on the Spec's Terms
A spec can state its modification conditions, which the resulting program checks against updates to decide which parts of it to apply, reject, and modify before applying, and then acts accordingly.
Rules about rules
A rule or larger specification can set the terms for its own amendment, as specifications are values the language reasons over.
A combination of properties no other language has
Tau computes rules so you catch any that conflict
Satisfiability is logically inferred rather than sampled, so the solver's output is fully guaranteed to be correct. Testing covers the cases written as tests; a decision procedure answers over the model as a whole.
Suitable outputs can be produced for every input sequence, without depending on future inputs.
Tau is built around a decidable specification logic. Its implementation checks supported specifications subject to practical resource limits.
A specification can reason over specifications
Tau Language has a type whose values are specifications, so a rule can set update conditions on the rules that may replace it. In other languages, a smart contract cannot hold another contract’s meaning, however they can with Tau.
Raising the spending limit takes 2 approvals. Changing this rule takes 3 approvals and a 30-day delay.
Revise specifications during execution
An update can be given as just an additional requirement. Tau can merge an update into a running specification, retain requirements that do not contradict the specification, and modify the update according to the specification before applying it.
A program can reject and selectively accept updates upon given rules.
Better software, built in a better way
A few examples of what is possible.
Systems that answer for themselves
Because the system is based in logic, questions about it are decided rather than estimated: what a rule permits, whether a change is safe, whether two rules can conflict.
Property — decidable, within the supported fragment
User-programmable systems
People using a system can change it by providing just the new requirements. The admission conditions are part of the specification rather than a separate approval process.
Property — a change is admitted only if it is satisfiable
High-assurance everything
An upgraded class of formal methods used in high-assurance systems, but applied to everyday software with Tau's properties. What must hold is decided before anything runs, rather than inferred from test coverage.
Property — decided, rather than sampled by tests
The better path to correctness
The differences below come from Tau's specification-first design, decidable reasoning, and runtime revision mechanisms.
Run the interpreter yourself
Start writing specifications with Tau Language now.
Read the research
Much of the research on Tau Language and its solver is public. Here are a few of the papers.