Tau 语言：软件合成的未来 [赞助] - Ohad Asor

Machine learning is a mathematical miracle. It can learn from examples and give correct answers with high probability for examples it has not seen, but this is only up to a certain probability. The error will never be zero, and accuracy gets better only up to a certain difficulty of problems. From a certain size of logical question, it will do no better than guessing.

You’re talking about the 3 curses of machine learning: the optimization curse, the statistical curse, and the approximation curse. You’re describing a completely different approach. Rather than doing statistics, we use a logical method to deduce an answer.

The T language is designed to achieve 1 and only 1 goal: to make software controlled by its users. Right now, users have very little control, if any. New blockchains come and go every day, but T is the end game of all blockchains. Every new idea that you want to incorporate into the blockchain—you just say it in T, and it will automatically become what you want it to become. You say it, and it will happen.

You tell the system, “Make a profit for me,” and it will make a profit for you, right?

Ohad, welcome to MLST. It’s such an honor to have you here.

Thank you very much. It’s my pleasure and honor.

Can you tell me a little bit about your background?

I’ve been a mathematician and software developer my whole life. I’ve been interested in various fields of mathematics, but in the last 15 years, mainly in the field of AI—at the beginning, machine learning and the theoretical foundations of machine learning, but in the last 10 years mainly in the intersection between logic, mathematics, and computer science.

What was the “aha” moment for you when you felt that this logical view of AI was really important?

I got familiar with the whole idea of mechanized reasoning. Normally, mathematicians view mathematical logic as a very boring subject, and I was no exception. But when I heard how algorithms can kick in and how logic can be mechanized by computers, this became really very interesting.

I’ve been going through your Twitter posts, Ohad, and in particular you’ve been talking about just how unreliable these approaches are. Tell me more.

Machine learning is a mathematical miracle. It is very surprising that it can do what it does, which is learn from examples and give correct answers with high probability for examples it has not seen—for out-of-sample instances. But this is only up to a certain probability. There is a certain probability that the error will be low enough; the error will never be zero, and the probability of zero error will never be 1. That’s why it is called PAC learning: probably approximately correct learning. You will probably be approximate, namely have low error, but that’s it. You will never get guarantees for absolute correctness.

Sometimes you need guarantees for absolute correctness. Moreover, sometimes you want to communicate with the machine in a way that is not effectively captured by examples. We are talking now; we are not only giving examples to each other. That would be crazy, and indeed it would be crazy to only give examples and expect to get true intelligence out of it. You need to say things, not only exemplify them.

It is very impressive that machine learning can do what it does by examples, but we are pretty much at the peak. It will not get much better than that. You need methods that are not machine learning, which will go beyond guessing from examples.

There’s always a bit of cognitive dissonance here for me. We’ve had Noam Chomsky, Gary Marcus, Judea Pearl, and many other famous symbolists on the show, and they’ve always said that reasoning without guarantees is not reasoning. OpenAI has been boiling the frog for the last few months with the o-series models. What we are seeing, even though these are statistical, empirical methods, is that the accuracy is going up and up and up. We can build engineering systems to make them better and better and better, and things just seem to be getting better. Everyone just seems to be accepting it. Why do we need to have these guarantees?

Accuracy gets better only up to a certain difficulty of problems. From a certain size of logical question, it will do no better than guessing. It will be completely random; it will be coin tosses.

For example, consider the Boolean satisfiability problem. You can imagine a set of constraints of the form, “If this guy comes to the party and this guy does not come to the party, then the third guy will come.” A set of constraints like this can be solved by SAT solvers with more than thousands of variables. But even o3, o30, or o300 will not be able, from a certain point—let’s say, hundreds of variables—to give a better-than-random answer. It will be coin tosses.

It’s not that, in 90% of SAT instances, it will return the correct answer. From a certain point, it will be random. One way to see it is through polynomial interpolation, like Lagrange interpolation. You can take any set of points and find the polynomial that fits this set of points. If you have 1,000 points, it will be a polynomial of degree 1,000. Will you be able to take a time series and fit it with a polynomial to predict the next time point? The prediction will be completely random.

This is captured by theoretical machine learning as infinite VC dimension. If you can fit infinitely many points using a polynomial of degree 3, that’s very surprising. It’s probably something fundamental about the nature of your setting, and then you have much more confidence that you will be able to predict the next points with good probability and low error. But if you just fit everything, this is what is called overfitting, and you will be random.

Intuitively, I agree with you. But what we’ve seen in the last 6 months, actually on François Chollet’s ARC challenge, is people leveraging transduction. That is simply a prediction function where the test-data specification is part of the prediction function.

Rather than having this inductive model, which memorizes all of the training set for the purpose of generalizing to any new, unseen example, this transductive approach embraces the situated complexity in the world. When a model needs to make a prediction, it incorporates situated knowledge inside the prediction function. It is a way of embracing the complexity that’s out there.

Of course, it is still just a new form of empiricist prediction, but it seems to be far more capable of making reasonable predictions in a given situation. Forgetting how you reach the prediction function, what your model is, and what your training set is, you just look at the end result. You can see right away the computational limitations of such prediction functions, no matter how you reach them.

If your concept class—the class of prediction functions—is all possible polynomials, as we said before, and you can fit everything, this class is too big. Its VC dimension is infinite, and there is no surprise that if you do interpolation over arbitrary data points, its prediction ability will be zero. It will be completely random.

If you take a smaller class, then if you fit your training data, you are not guaranteed to fit it. But if you fit it, then you have a lot more confidence—not a guarantee—that you will fit out of sample well.

This is interesting. You’re talking about the 3 curses of machine learning: the optimization curse, the statistical curse, and the approximation curse. We can choose a smaller hypothesis space, and if it’s too coarse, we get approximation error. We have the statistical error, of course, which is fitting a statistical model to this class of functions. You’re describing a completely different approach. Rather than doing statistics, we use a logical method to deduce an answer. What’s the trade-off? What do we lose by having a logical methodology instead of a statistical one?

One thing is that the information has to be there. If all your information is examples, that’s not enough. You need to actually say the thing.

Machine learning is good precisely for cases when you don’t know how to say the thing. For example, face recognition: no one can put into words what a face looks like. You can see and tell right away, but you cannot put it into words. For things you cannot define, machine learning is very good. But for things that you can define, go ahead and define them. Why go by example?

Is it possible, though, that this is a kind of dichotomization? Many people say machine learning is great for things that I can’t write code to do. I can’t write code to recognize a face, a cat, or a digit. There are many things in the world that we can describe logically using language, but isn’t that too much of a separation? Aren’t there situations where we could decompose face recognition into a program, or combine pattern recognition and logical reasoning into some amalgamated form? Does it make sense to think of them as 2 completely distinct domains?

Before speaking about computers, there is a big dichotomy between the world and the things that we say about the world. The things that we say about the world are just things that we say. The finger pointing to the Moon is not the Moon; there is a very big difference.

This dichotomy is already there. As human beings, we are obsessed with living in the world of language—the conceptual world, the things that we say about the world. Language is even more central to our lives. We’ve left the real, physical world here. What are we doing right now? We are talking, right? For us, this is actually doing something, but we are only talking. There is nothing wrong with that. That’s our human nature. We live in the world of concepts, in the world of language.

Let me extend that a little bit. Knowledge is a justified, true belief, and what we need to do is reason about knowledge that we actually know to be real. What’s happening with the machine-learning world at the moment is that we are being possibly gaslighted into thinking that reasoning is more general than what the Greeks thought.

There was a famous Monty Python sketch where they were asking whether someone was a witch. People said she was a witch because she got out of bed on this side, had a pointy nose, funny hair, or something like that. This sounds like reasoning because we’re constructing all of these different rules and composing them together, but there’s no surface contact with reality.

You’re right. This dichotomy between the world and the things that we say about the world means that they are pretty much disconnected. To demonstrate this, we cannot even define what it means to physically exist. If we cannot define that, then how can we define anything else in the real world? Even existence—we don’t know how to put it into words.

There is a very serious dichotomy between language and the world. However, in our human experience, language is as real as the world, if not even more real. If we were some different kind of creature—aliens that may be very advanced but are not obsessed with language the way we are—then maybe logic wouldn’t be interesting. But we are humans. We reason using language, and that’s why it is so relevant for us.

You said that language feels very real to us, but there’s a phenomenal component of real and then there’s an epistemic component of real. Certainly, many of the things that we talk about in language we know to be true. They are facts, things that exist, cities that are placed in a certain country. I suppose there’s a spectrum beyond that of things that we just feel to be true.

Of course, as humans, we have some connection to the real world. But when you say, “I will go to the shop to buy tomatoes,” the tomato is only a word. It is not connected to the physical tomato that is there in the shop. You have no idea what that physical tomato in the shop is. You cannot even point to it until you reach the shop and take it. Until then, you have the idea of a tomato and nothing more than that.

I also say about myself that I’m a mathematician. It is just a word. In reality, I’m a guy with glasses and no hair. That’s what I am in reality. “Mathematician” is only a word, but that’s what matters to us as human beings. We live in the world of language.

In which case, there is a potential divergence between the words we use, what they mean, and how they correspond to the real world. The concept of a tomato is an example of abstraction. It’s a category that has formed over possibly a constructivist evolution of language use—or maybe it’s just a fact of the matter about the universe. How did that concept come about?

Language can somehow point to the world, but it can never touch it. To show you that it can never touch it, let’s return to the question we asked before: can you define what it means to physically exist? No one can. If you cannot define physical existence or put it into language, then you cannot put everything else into language either.

All you can do is approximately point, but never touch.

What does it mean, then, to build AI systems when, even by your own description, there is little surface contact with reality—even in the most formal descriptions of things?

What we are really interested in is not reality, but reality as perceived by us. We perceive things largely through language, and this we can implement in a computer. Moreover, how are we going to communicate with a computer? Through language, because we are creatures of language.

It is much less about the world as it is and much more about human nature. We want computers to serve us as humans, given our very peculiar human nature.

The only potential objection is that I think of language as a living organism that supervenes on us. It rests on us; it’s always adapting and changing. When you extract a formalism—because natural language isn’t a formal language—and put it into an AI system, wouldn’t it very quickly diverge from the language that we use and know?

It will. When I say “language,” I’m not pointing to any specific language. I’m referring to the abstract concept of saying things and expressing things in a symbolic way, like letters—or not always letters, and not only letters.

If you ask me where something is and I tell you, “It’s there,” that is also language. It is a sign that describes something, whether real or completely abstract. I am by no means referring to the specific nature of a specific language. I’m talking about the general idea of abstraction.

There seems to be a relationship between symbol use and abstraction in general. Humans are different from all other animals because we have this declarative labeling ability. We have this plasticity in how we can point to things, give them labels, and share those labels with other people. The use of those labels gives rise to abstraction.

Certainly, machine-learning models don’t do symbols and abstraction without hacking. We can wire them into a recursive loop, give them chain-of-thought, and make them act as if they are doing symbol-like things, but it’s not very natural. It comes very naturally to us, doesn’t it?

Yes. If you want to do logical reasoning, why go so indirectly and encode it in linear algebra instead of directly doing logic?

The big thing that you’re advocating for is verification—being able to have guarantees.

I think verification is old news. The real deal is synthesis and verification.

In verification, you describe a system and statements about the system, and then you verify that the system meets those statements. In synthesis, you describe only the statements about the system—the requirements—and then you automatically generate a system that meets those requirements.

One way to look at it is the common practice of programmers writing tests. Tests are programs that test your main program and make sure that it returns the right answer. To demonstrate synthesis, imagine that you write only the test, and then the computer automatically synthesizes a program that will make the test pass.

There must be some kind of erroneous behavior that my smartphone might exhibit that we want to guard against. Within our system of—well, we call them tests, but of course we’re talking about epistemic tests, not statistical tests—when we describe the behavior of the smartphone, it needs to make sense. What does it mean for a test to make sense?

Let’s say I want to make sure that the phone will never send my passwords over the network. A test for that, which you cannot implement in reality in the way I’m going to say it, would be: try all possible inputs for the phone—all infinitely many possible inputs—and check whether, at one point, it sends your password over the internet. If it does, the test fails.

How are you going to test something over an infinite domain? By the magic of mathematics. Sometimes in mathematics, you can prove something about all infinitely many numbers. If you describe this test-and-synthesis problem in the right mathematical framework, you can give guarantees about all infinitely many possible inputs.

Playing devil’s advocate, we see an interesting phenomenon on Instagram, Twitter, and elsewhere. There are all of these constraints—you’re not allowed to refer to women, for example—and people get around the filters by using new language terms to describe females. Isn’t it the same with a password? I could encode the password in an infinite number of ways, and wouldn’t that allow me to circumvent the system?

That’s right, you could, but it was only an example. Let’s say that you don’t send the password in clear text. Even then, how are you going to do that? That isn’t the point of the example. The point is that you want to say something about all possible configurations of the system and all possible inputs, which are basically infinitely many. To get a guarantee for that, you need very specific mathematical frameworks.

But doesn’t that just create an infinite regress? We wouldn’t be able to describe the uncountably many ways that people could send a password. I could give you an idea: someone might come up with a new term for women—“calcium cannons,” for example—and any reasonable language user would be able to perform inference in that situation and say, “That’s what they mean.”

Wouldn’t we have a similar issue with facial recognition? I can’t write code to do facial recognition because people’s faces are changing all the time. There is always an exception that breaks the rule. What we’re doing is using a logical framework to describe an amorphous, living thing, and it needs to adapt continuously.

There are 3 moving parts here: the computer world, the human world, and the physical world. I know how to treat the computer world. How to treat the human world or the physical world is beyond me.

I can give you guarantees about what the computer is going to do. For example, suppose you want to start your own bank and need software for your bank. You want to say, “No balance can be below zero unless it is authorized.” You really want this; you really need this. How are you going to do it? Are you going to ask o3 to give you your bank software? Let’s be real: even the biggest LLM proponents would never imagine doing such a thing. You really cannot trust this.

What are you going to do? Traditional programming. That’s what people really do. But then how can you make sure that the balance really is never negative? You need to go over all the places in the code where the balance is updated, implicitly or explicitly, and make sure that it is not negative without authorization.

In the synthesis-from-requirements approach, you simply put in the sentence, “Balance greater than or equal to zero,” and that’s it.

That makes sense. But isn’t there always an exception? Let’s say that next Friday there’s an interesting case where a banker from Zurich has a special arrangement with the bank, so he’s allowed to go below zero under these conditions, but no one else is allowed to.

I can imagine a world where we decompose things into pockets of regularity—situations that can be rigidly defined—and the rest is just chaos. I can see specific situations where we could build systems like this, but sometimes we need to have flexibility as well.

Now you are going a step forward, from writing software into how software changes. That is, of course, also very important—no less important. Indeed, the synthesis framework that we work on in the T project heavily involves how software is updated.

Maybe we should get to that in a little while. Coming back to a few interesting questions, you haven’t been influenced by Kurt Gödel or Alfred Tarski?

Not really. What does it mean to be influenced? When I open a mathematics book—that’s something I do regularly—of course I’m influenced by the things written there. But I cannot say that Tarski changed my course of action.

It did turn out that our courses—the big Tarski’s and the small me’s—had some similarities, but I discovered this only in retrospect.

Would it be fair to say that you think Tarski is one of the best logicians of the 20th century? Everyone would agree with that statement. In which case, why would you not say you were influenced by him?

So your journey into this world was very much self-guided, and then afterwards you contextualized it?

Yes. I’m always very original, and not always right, and not always bright, but always very original.

Is that a better approach than first looking at what’s out there and being influenced? Do you think it’s better to do it from first principles?

I always start with the literature. I never try to do things from first principles if I can find sources that can help me and continue from there. Sometimes there is no choice. When I needed to have a language that could refer to other sentences in the same language, there was absolutely nothing out there. I had to do it from scratch.

You’ve also said that pure logic-based AI isn’t essential for safety. What gives you the conviction to say that?

That’s not exactly what I said. I said that a language that can refer to sentences in the same language is essential for safe AI. That’s the key point.

Conventional logical AI and conventional logical frameworks, which are not machine learning, also cannot do this without the component that makes it possible.

So there is a specific form of logical AI in which a language can refer to its own sentences.

Yes. I’m the only one to discover this.

That specific form of logical AI is essential for AI safety?

Specifically, in logic, in general, there is no logical language that can do it. This is achieved by abstracting sentences into Boolean algebra elements.

The core of what we’re talking about is that in the 1980s there was the notion of the expert-systems knowledge-engineering bottleneck. People were building systems that described the world using a series of rules and logical language.

The problem was similar to the difficulty of using code for facial recognition. These people started building ontological frameworks to describe domain-specific systems in the enterprise, and they found that a form of brittleness emerged. They always needed to put in more and more and more special cases. How is your system different from that?

That’s very simple. I have no intention of describing the whole real world. I intend to make computers do what you want them to do.

To accurately describe the world is too much, and it is not necessary. We want to describe the things we are interested in to achieve our human goals.

Does that mean there is a class of domain-specific systems, such as safely flying a plane, that we could describe using a logical framework, but there might be other classes of things—such as ensuring that people don’t post racist remarks on a social-media site—that might be beyond the capability? Where do you draw the line?

Programming languages can express anything that a computer can do.

You could ask me, “If they can do anything, please write me a program that detects racist statements on social media.” If I promised anything, you can come and ask me to do anything. The answer is that you can do anything as long as you know what you want. If you can give an accurate description or a definition of what you want, then you can achieve it.

If you cannot come up with the definition, then maybe choose machine learning. You can give examples and get a less accurate system, but it is better than nothing.

What is the bright line between things that we can describe in language and things that we can’t?

I can understand this question in 3 flavors. The whole field of mathematical logic speaks about which mathematical structures you can define in language. Here you can have a simple countable–uncountable argument.

A language contains sentences, and each sentence is a finite sequence of symbols from a finite alphabet. There are always only countably many sentences, while mathematical realities go way beyond countable cardinality. Of course, not every mathematical structure is definable. In fact, very few of them are.

The second flavor is what is computable. We have computability theory and complexity theory, and we can speak about what is computable and what is not. We know, for example, that the halting problem is not computable. There are computable numbers—of course, only countably many computable numbers—but the real numbers are uncountable. Almost all real numbers are uncomputable. If you choose a real number at random, then with probability 1 it will be uncomputable.

The third flavor is what we can define in the real world using language. This goes back to what I told you before: if we cannot even define what it means to physically exist, then the answer is nothing. Nothing in the real world can be defined. Maybe you can approximate it. Maybe you can give a definition that is good enough for another human being to understand what you mean. If you tell someone, “Get me tomatoes from the shop,” they can do that, but it is not a definition of the physical tomato in the shop.

You’re saying that, subject to the constraints of definability, computability, and language, there exists a subset of problems amenable to this kind of logical description.

Yes. The most practical area of interest is probably defining what computers should do—defining programs by logical means.

Going back to the bank example, you want to say that the balance should never be negative. You want to say, “Balance greater than or equal to zero,” and that’s all. You don’t want to go over the whole control flow of the program and check whether the balance can become zero. You just want to put in this constraint and be guaranteed that it will be met.

Another thing you’ve said is that in the last 20 years or so there have been advances in computation that make this more plausible and more realistic. Can you tell me about that?

The big AI winter in the 1970s was all about logical AI. It came from the Lighthill debate, which is available on YouTube. I recommend everyone watch it. You can see Sir James Lighthill lecturing and recommending to the British government that, because of the complexity of logical reasoning, they should defund AI, and in particular logical AI.

At the time, the class of problems called NP-complete problems—where even the most basic logical questions are at least NP-hard—was believed to be absolutely intractable. It was thought that even small NP-complete problems would never be solvable. Up until today, there was no theoretical proof of that; it was a belief that turned out to be wrong.

Now we have an empirical proof, not a mathematical proof, that even very large SAT problems can be solved very quickly. Over the last 20 or 30 years, the field of SAT solvers has suddenly started surprising researchers by showing that what they believed could not be done can be done quite easily.

There is almost a Moore’s law of SAT solvers: they just become better and better, and they continue to improve. We have empirical evidence that logical reasoning is feasible in practice, in contrast to what was thought before. That’s why the time to invest in and research logical AI is right now. We now know that abandoning it was a mistake. It was not abandoned because it was not good or promising; it was simply thought to be too difficult.

It was a similar thing with deep learning. Everyone wrote it off in the 1980s, and then suddenly we had all of these GPUs, algorithmic tweaks, data, and so on, and it became tractable.

You’re talking about constraint-satisfaction problems. What are the key improvements that have made them tractable?

It is boring stuff. It is a combination of an algorithm called DPLL with another algorithm called CDCL. It eventually turned out, for reasons that no one knows, to solve SAT very fast.

It is basically a bunch of quite trivial heuristics that no one thought would solve difficult problems, but it turned out that they did.

Do you see a potential hybrid between deep-learning systems and logic-based systems, or are you advocating purely for using logic-based AI in specific scenarios?

I advocate for purely using logic, and whenever statistical reasoning or machine-learning reasoning is required, expressing it in logic. After all, if you open a machine-learning book, it is written in logic—in something equivalent to logic programs. Programs that do machine learning are programs; they have their own logic.

I advocate implementing machine learning inside logic.

What does it mean to implement machine learning inside logic?

You can describe any machine-learning algorithm in logical languages. Then you get the benefit that this logical description lives inside a broader logical description. It is just part of the whole thing that you are doing. You can augment it with guessing and machine-learning capabilities.

So pragmatically, you’re saying we can combine the 2 modalities by almost creating a compiler. We describe what the machine-learning problem is using the logical language, and then we generate or synthesize the machine-learning framework, but still within the construct of logical AI.

Yes. If all you want to do is machine learning, then do machine learning. But it never comes in a vacuum. Imagine our bank software. It is mostly not about machine learning and mostly not about guessing. Sometimes you want to do some guessing; then express that method inside your logic.

That means we could use the logical framework as a form of verification alongside a machine-learning algorithm.

Logic is a form of description. What you do with the description—whether you verify or synthesize—is a different question.

Normally, machine learning does not come in a vacuum. You want to describe some system where machine learning is part of it; it is not all of it. In logic, you can do that. You can describe your whole system, including the machine-learning part.

What you’re saying is that the logical language is the source of truth. It’s similar to the object-relational mappers for building databases. They might say that code is the way we describe database models, so we don’t want anyone building databases directly. There are no SQL statements; no one talks directly to the database server. We describe database-access code using C++ or some other language, and we abstract away the database.

You’re saying we abstract away all of the machinations of the software. All we need to do is describe it with logical language: describe the requirements, the “what,” and not the “how.”

You describe the test that the software has to pass. You don’t need to describe the software itself.

This seems like a galaxy-brain idea. We can describe declaratively what the software does. Why is there not an infinite space of possible implementations that could be synthesized from those requirements?

There is an infinite space. Normally there will be infinitely many programs that meet your specification. If you are fine with the backend eventually choosing one arbitrarily, then that is good. If you are not fine with it, you have to put more constraints in your specification.

Are you describing a workflow where we create the requirements, synthesize 1 of the infinite number of possible implementations, observe the behavior, and already know that the program is correct because the whole point of your system is that it is correct given the requirements? At what point do we realize that we need to make a change?

Either you had a bug in your specification—you wanted to specify something but did not—or reality changed and you want to adapt to reality.

I suppose that might happen in 1 of 2 ways. We might realize that our specification has changed, or we might see from the behavior that we didn’t get the specification right in the first place.

Yes, of course.

Can you explain in simple terms how it is possible to create a program automatically from a set of requirements? So many people are trying to do program synthesis, and the naïve way is to have an exhaustive, exponential search over the space of programs. I’m guessing that’s not what you do.

No, because the space is infinite, so no exhaustive search can cover all the options. For this, you need a mathematical framework where you can make statements about infinitely many objects in your framework quite easily.

As an example from a different field of mathematics, if you have a nonconstant polynomial over the complex numbers, you know that it has a zero. That is the fundamental theorem of algebra. You don’t need to check all infinitely many complex numbers; you are guaranteed that it has a zero.

A similar thing happens in the mathematical framework of the T language. You make statements about infinitely many sentences, and by relatively simple checks you can get a guarantee that something exists. You can even get an algorithm for how to obtain 1 example of this thing.

Let’s give a very simple example that is not about the T language. Suppose you have to output a number, and you say that the number has to be bigger than 10. There are infinitely many numbers bigger than 10. How are you going to choose? That’s not so hard. Just because the search space is infinite does not mean it is impossible.

How did you overcome Tarski’s undefinability of truth in defining your language?

I identified the real-life necessity of having a language that can speak about its own sentences beforehand. I don’t think anyone had identified the practical need for it. They saw it as a philosophical gadget.

Tarski proved that, in a certain setting, it is really impossible—in a certain very broad setting. But because of the practical necessity, I tried by all means to find a way to do it in a way that is good enough in practice. The way I found was to abstract sentences so that they are only Boolean-algebra elements. We forget about the structure of the sentence and look at it only as a Boolean-algebra element. Then it all works.

Maybe we should introduce Boolean algebra and Tarski’s undefinability theorem for the audience.

Tarski’s undefinability of truth says that if you take the language of arithmetic for the natural numbers, with addition and multiplication—and, of course, any language that contains this language—and add a truth predicate, you get a contradiction.

What is the truth predicate? It is something that takes a number—after all, it is a theory of numbers—and that number is an encoding of another sentence in this language, the language of arithmetic with a truth predicate. This kind of encoding of sentences is called a Gödel number.

The truth predicate gets the Gödel number of a sentence and tells you whether that statement is true or false. Tarski does not ask you to implement this truth predicate. He only assumes that it exists in your language, and from this assumption he is able to recover a contradiction.

A language like this will be inconsistent. You will be able to prove every statement and its negation.

What is Boolean algebra?

There are 2 ways to define Boolean algebras. One way is that a Boolean algebra is a collection of sentences where the operations defined between the sentences are “and,” “or,” and “not.” Those are the only operations.

Another definition is that a Boolean algebra is a collection of sets where the only things you can do with those sets are union, intersection, and complementation. Most importantly, you do not have the membership predicate. You cannot look at the elements inside the set. You have only union, intersection, complementation, and equality.

In the sentence definition, equality would mean semantic equality—whether the sentences mean the same thing, not necessarily whether they are written in the same way. That is a Boolean algebra.

The theory of Boolean algebra has the quantifiers “for all” and “there exists,” along with “and,” “or,” “not,” and equality.

How do you compute whether 2 Boolean algebras mean the same thing?

You don’t. You take it for granted.

If you want to work with the language of Boolean algebra over some Boolean algebra of choice, you need to implement that Boolean algebra of choice. You need to give me “and,” “or,” “not,” and equality. If you give me that, I can take a sentence in the language of Boolean algebra and tell you whether it is true or false in your Boolean algebra.

You’ve defined—or invented—the T language, and it overcomes Tarski’s undefinability theorem by allowing it to refer to its own sentences. You’ve abstracted sentences into Boolean-algebra elements. Can you talk about some of the fundamental building blocks? There are simple Boolean functions, Boolean functions, and pointwise revision. How do all of these things operate in the T language?

The T language is the standard theory of Boolean algebra with certain extensions.

The first extension is that in this language you can write any Boolean-algebra element. In the standard theory of Boolean algebra, the only things you can refer to directly are 0 and 1. In this extended theory of Boolean algebra, you can refer to any element.

The second extension is that the Boolean algebra it is talking about is nothing but the Boolean algebra of T sentences itself.

The third extension is the temporal dimension. When we speak about Boolean-algebra elements, we speak about how they evolve over time. You can say, “This statement now compared to the statement 5 steps ago.”

There is not only a temporal dimension; there is also a distinction between inputs and outputs. This distinction, the temporal dimension, and the inputs and outputs are necessary to make the language a software-specification language.

This distinction between inputs and outputs is a very strong property because in the T language you can prove that, at each point in time, for all inputs there exists an output that meets the specification. This is not something you can do in other specification languages. You can do it only if your inputs and outputs come from a fixed finite domain. Here, the domain is infinite: the domain is all T sentences.

Pointwise revision is about how to update T programs if you want to change your specification in live software—how to incorporate only the change and keep everything else intact.

The first thing is that we’ve created an algebra that can, for any point in time and any input, guarantee that the output matches the specification.

It can check. You have your specification, and maybe your specification does not satisfy “for all inputs there exists an output that meets the specification.” We can check your specification, and that is what we mean when we say the specification is satisfiable.

If your specification is satisfiable, then we can synthesize a program that meets it.

How do you take that step? How do you synthesize a program from a Boolean algebra?

This is very complex. At the beginning, I knew how to make an interpreter but not a compiler. I could execute your specification, but I couldn’t put a program on the table for you to run. I could still execute it, and that was not trivial at all.

In fact, I finalized the full synthesis algorithm only about a month ago. Now I know how to put the whole program on the table.

Can you tell me about that? Does your system support—I'm just imagining here—generating C++ code and then compiling it?

Yes. There is almost a transpilation process. In principle, it does not have to be C++; it could be any Turing-complete language.

Have you gone with C++? What guided your decision?

In the company, we work with C++, and I am a fan of C++, so it will be in C++.

Right now, we have implemented the interpreter, which can execute a specification, but we have not implemented the synthesis yet.

Is there a situation where efficiency isn’t respected? For example, I train a deep-learning model to recognize a face and it works, but it’s hideously inefficient. It has generated some strange, galaxy-brain circuit. Is there a situation here where, when you generate a program, it isn’t necessarily the most parsimonious program?

Yes, it is a big difficulty, and it will be an ongoing effort. I do know how to identify cases in which things can be executed fast. Moreover, the user—the person who writes the specification—can write it in a form that will be executed fast.

There is also the possibility of using SAT or SMT solvers, although it is not clear at this point that this will make things better. There is, of course, an ongoing optimization effort.

I guess it will mainly come down to identifying the easy cases and synthesizing functions that do not need to perform logical solving. You do the logical solving beforehand, and you output a straightforward function that just takes the input and gives you the output.

Is there a relationship between the complexity of the requirements and the complexity of the generated program?

Yes, of course. Not in all cases. Sometimes you can take something very simple and write it in a very complex specification. But if you speak asymptotically, as the size of the specification grows to infinity, in the worst case the complexity of the program will also go to infinity. The answer is obviously yes.

There’s a huge skill component, then, to defining the requirements in such a way as to collapse as much complexity as possible before you compile the program.

Yes, but it is helped by the very strong simplification algorithms that can be implemented.

Would these simplification algorithms be implemented at the compiler level or at the requirements level? You might be able to identify certain patterns of bad design. I place these requirements into the T language, and you might rewrite them to be more efficient, but then perhaps they are less intelligible to the person who wrote the requirements. What’s the trade-off?

When we normalize or simplify formal statements, they might become less intelligible. Sometimes they do; sometimes they do not. If you take a very large specification and normalize it into 1 line, that’s very nice, but it will not always be the case.

Human readability and explainability will be an ongoing effort.

I suppose that sketches out a future where we should think of the T language as a kind of interface. At the interface point, it needs to be maximally legible to humans. There might then be an intermediate minification or normalization step, followed by another compilation step where the program is optimized again.

That’s how it works.

One of the really cool things you’ve done is this concept of pointwise revision. That allows you to change the system while respecting as much of the old specification as possible. How does that work?

Generally, the revision problem is unsolvable. There is a whole field called belief revision that speaks about this impossibility.

For example, if your old knowledge base says “A implies C” or “B implies C,” and now you want to revise it with new knowledge that says “Not C,” you have several options. You can delete the law “A implies C,” delete “B implies C,” say “Not A,” or say “Not B.” There are many ways, and there is no way to choose one optimally.

Revision is really impossible. But in a certain setting, it is possible in a very clean and optimal way: the setting of the T language, which is a software-specification language.

If we focus on what matters—and what matters is what output the program should produce now, at each point in time—we can perform the optimal revision. You simply write a T formula that says, “If there exists an output that satisfies both the old and new specifications, choose it. If such an output does not exist, choose one that satisfies only the new specification.” That’s all there is to it.

Pointwise revision is one of those things that, when you see the answer, looks very easy. Before you see the answer, it is really very hard.

Suppose you have a big program with a lot of moving parts and features, and you want to change only 1 small thing in 1 specific component. Do you need to write the whole software from scratch?

No. You write only the thing that you want to be new, and the rest will remain intact.

One of the advantages of the logic-based approach is global consistency. This is the idea that here is the system, and this is what it does in all situations.

When you start placing—I’ll use the word “local”—rules into it, saying that in this time and situation you do this, otherwise you do that, doesn’t that create illegibility? Doesn’t it make it harder for people to understand as a whole what the thing does?

A partial remedy is the normalization process. For example, in pointwise revision I said, “If there exists an output that satisfies both.” The key word here is “exists.” In logic, this is called a logical quantifier.

In atomless Boolean algebra, we have quantifier elimination, so we know how to make this “exists” disappear. That is only 1 example. During the normalization process, everything will be crunched together and all redundancies will be removed, so it will be more intelligible.

I cannot tell you that it will be fully intelligible, but no one can mathematically define what it means to be intelligible. If you could define it, then we could implement it. No one can define it.

But then you’re essentially rewriting the rules. Doesn’t that mean the humans who created the specification have it transformed into a slightly alien form that they no longer recognize?

Yes, it can happen. It happens all the time in standard programming, and it is something to mitigate. There is no magic solution.

In normal software programming, there’s a cognitive interface between software engineers and what the computer does. We come up with high-level abstractions. We might use the mediator pattern, the observer pattern, or other design patterns. Weirdly, the way the code actually works on the computer doesn’t resemble those abstract patterns very much at all. It’s just a cognitive interface.

It would be very strange if my Python interpreter rewrote my code for me and said, “Actually, this is the way I’m going to represent your code,” because that would mean my provenance—my mental journey of getting to that place—had been scrubbed. I couldn’t then make subsequent steps in that cognitive space.

The Python interpreter does rewrite the code for you. It just doesn’t show it to you, but it does.

I see. You’re talking about rewriting the code while still maintaining the rules as the developer created them.

Again, it’s your choice. The way Python rewrites your code is always horrible; you never want it in that form. But the way we rewrite your T specification can sometimes be even better than how you wrote it initially.

What I’m getting to is that when a C++ compiler optimizes code to make algorithms run faster, the optimizations always seem very alien to us. Are you making the argument that optimizations in this language space can actually seem even better to us than the original thing we came up with?

They can be. Not always, but sometimes.

One example I already gave you is quantifier elimination. All the “for all” and “there exists” statements that you write can be made to disappear.

How do you see the T language being incrementally adopted in existing software-development workflows? Let’s imagine that we’re not going to throw everything out and start again. We’re going to incrementally adopt it inside systems and subsystems. How might that look?

The T language is designed to achieve 1 and only 1 goal: to make software controlled by its users.

Software is there for 1 thing: the users. How can users control the behavior of the software and change it over time? Right now, they have very little control, if any. If you want software to be controlled by its users, you will need to use T technology. You have no other choice.

It all comes down to what we spoke about: software specification and pointwise revision. The user can say, “I want this to hold,” and the whole specification will remain intact except for the part the user wants to change.

This makes a lot of sense. I suppose there’s an ideological component here. You’re a fan of decentralization and allowing the people who use software to control it. At the moment, we have centralized teams of developers who decide what features to build into software. You’re saying that in the future we’ll have software actually written by the users who use it.

Yes. Moreover, it is not only about decentralization. I am the user; I am the boss of my computer. I decide what runs on my computer. Why should other people decide for me? I want this power.

How could that work? One way is that you write your own software that runs on your computer. But if we broaden out a little, there could be software that you share—you’re a user, and thousands of other people are users—and you collectively improve that software. You decide collectively what the best new features are to add, and there is some kind of coherence mechanism. New requirements get added over time. How does that work?

That is another step, and it is also very fundamental to the whole Tau project: software collectively controlled by all of its users. In particular, a peer-to-peer network or blockchain network controlled by all its users.

What is the alternative? The alternative is what we already have today: a blockchain network and an economy controlled by a small group of developers. How can that have broad enough shoulders to support a real economy? It simply doesn’t.

I’m not saying that the other extreme is the way to go. I’m not saying it should be controlled by all its users in a completely equal manner. Maybe it should be some kind of meritocracy; I don’t know.

For this reason, we invested a lot of effort in formalizing laws for changing the laws: how to change not only the program, but also the way that program is changed. Only when the governance mechanism governs itself can you have a way to change the governance mechanism itself.

Only in this way can you have a blockchain network that can reliably support an economy in the wider sense—an economy that lives in society. It is not just a coin in a vacuum. There is a whole society, a whole market, and a whole economy around currency.

There are 2 components here. The first is using the blockchain to create a decentralized, coherence- or consensus-based approach to writing software. It’s not that Tau uses blockchain; blockchain uses Tau. Blockchain needs Tau.

The blockchain needs to be redefined over time by its users, and like any other software, you cannot have software that is defined in a sound way by its users without Tau technology.

The blockchain needs Tau to be redefined over time by the users.

You’re saying to use the Tau language to define the blockchain.

Yes.

We use the Tau language to define the blockchain, and there’s some kind of consensus algorithm that could itself be defined with the Tau language. What is the currency? A blockchain has a coin and a currency. How is that related to everything we’ve just been discussing?

When we say “software controlled by its users,” the software has to do something. It is not only controlled by its users; it has to do something, and that thing is also controlled by the users.

In blockchain, that is what it does: cryptocurrency in a way that is controlled by the users. If you want to change how the cryptocurrency behaves, or if you want to make it do other things, you can.

Smart contracts are just 1 aspect of users controlling the system. As a user controlling the blockchain, you say, “I want this behavior to take place,” and it will take place.

Before, we were talking about using the Tau language to create specifications for software that is synthesized. Now we’re talking about using the Tau language to decide collectively, in a blockchain network, how the blockchain network is transacted.

Is there an intersection between those 2 things? Are we designing new ways of controlling blockchains, or are we using the Tau language to create new types of software?

To create new types of software, in particular this blockchain software. One is a special case of the other.

New blockchains come and go every day because they supposedly offer this feature or that feature that wasn’t offered before. Where is it going to end? There are thousands of blockchains. Where does it end?

It ends with a blockchain that, however you want to change it, will change on the fly. That’s why I wrote an article on Twitter saying that Tau is the end game of all blockchains.

Every new idea that you want to incorporate into the blockchain—you just say it in Tau, and it will automatically become what you want it to become.

One use case you mentioned is trading knowledge. In the same way that you can say anything about the software controlling the software as a user, one of your statements could be: “If someone sends me an answer to this question”—and you would have to define what it means to be an answer to a certain question—“then I will give them coins.”

You just say it, and it will happen.

Another concept is the automatic businessman. You say, “These are the assets that I have. These are the things that I want. These are the deals I’m willing to take part in.” You don’t even have to say it explicitly; you can say it implicitly. Then you tell the system, “Make a profit for me,” and it will make a profit for you, of course whenever possible.

The concept of an automatic businessman—that’s strong stuff, and that’s only 1 aspect.

Many in the audience might not know much about blockchain technology in general. To make it clear, the technology is perhaps the most efficient form of structured financialization. You can create markets, and many people have used smart contracts before. You have certain guarantees: here is a piece of software that runs on the blockchain with certain guarantees, and it is decentralized, so we have this web of trust.

You’re saying that with the Tau language, we can adapt the blockchain and make it do what we want while retaining the guarantees we had before with blockchain technology.

Yes. To contrast Tau with other blockchains that support smart contracts, smart contracts can be updatable in the sense that you can replace the contract with another contract. But it is still not the case that the code of the blockchain itself is a contract. In Tau, they are at the same level; they are the same thing.

The second difference is that existing smart-contract languages are just programming languages. They are not specification languages that can speak about other sentences in the same language.

In the Tau language, you could have a contract that says, “The balance can never be zero.” You don’t have to go over the whole flow. You can also say, “If some other contract implies a certain reality, then do this and that.” Those are 2 major differences between the smart-contract aspect of Tau and traditional blockchains.

Very broadly, are you saying it’s a type of meta-blockchain?

Yes. Tau is its own metalanguage because it speaks about its own sentences. In a metalanguage, people usually speak about the metalanguage and the object language. The metalanguage can do basically anything it wants with the object language, but Tau’s own metalanguage is restricted to Boolean algebra. That is the only thing it can do with itself.

The Tau blockchain is its own meta-blockchain.

This is making a lot of sense. You’re saying the reason we have this proliferation of blockchains is that they are essentially handcrafted. People decide, “I’m going to code these smart contracts,” and they write them with code. There is a kind of brittleness.

You’re talking about a blockchain that has not only a metaprogramming and amorphous capability, but whose behavior is controlled by its users.

Yes, that’s right.

That’s what you’ve built.

It’s still not ready, but it’s almost ready.

When are you going to roll this out?

That’s a good question. I don’t want to make any promises. I was too optimistic in the past; I thought it would already be ready by now, but unfortunately it is not ready yet.

The hard parts are behind us. I’m sure you can appreciate that the hard part is implementing the engine of the Tau language. That is ready to a large extent. There is still more work to do, but the hardest part of this hard part is over.

I don’t want to give any specific time estimate, but it is coming.

Do you see this as the single blockchain to rule them all, or do you think there will be many Tau blockchains?

Because it is controlled by the users, the users will also set the incentives. I expect users to disincentivize forking and incentivize keeping everything in the same place.

When you launch this new blockchain, will people be able to buy tokens?

People can already buy tokens. There is the Agoras token, AGRS. When we launch the system, users will be able to control all aspects of the blockchain and the token.

People can already buy it, then. The blockchain is being launched, but it doesn’t have the new software running on it.

The blockchain is not launched. There is currently a temporary token implemented over Ethereum that will be swapped to the full token when the blockchain is ready. What people can buy right now is the temporary token that will be swapped.

What do you think about the angle of collective intelligence? Do you think it is possible, using a system like Tau when implemented in the blockchain, to solve problems that individual brains can’t solve? There’s a collective-work angle to solving big problems.

It’s like software development. There is a famous quote that what 1 developer can do in 1 month, 2 developers can do in 2 months, because development doesn’t scale. But there is more brain power.

Imagine many thousands or millions of developers in a way that can scale. They just state the requirement, and the system crunches it all together. Of course, we are going to get software of a scale and quality never seen before.

What happens when people vehemently disagree with each other?

It all depends on the laws for changing the laws, which is yet another thing to be decided over the system.

Do you think there could be a social benefit to a system like this? Right now, we have echo chambers, and people are not really aware of their logical contradictions. Do you think a system like this could help us get closer to various truths in the world?

What it more directly brings us to achieve is a computer that does what we want it to do. Computers already do things that we want them to do, but not everything and not perfectly. Tau will take software to the next level of satisfying the users.

What does it mean to be good software? It means to do what the user wants. That’s what it means. To be better software means to do more of what the user wants.

What would be the best software? The best software would be software that the user tells what to do and it does it. By this definition, which is not so crazy, Tau is the best software. It will just do what the user wants it to do.

Steve Jobs famously said that people would want faster horses and that people don’t know what they want. What do you think about that?

It is true. The definition I gave is a bit simplistic, but it is already a big deal.

Maybe we’re not giving users enough credit. If users actually had interactive control over the requirements that generated the software, maybe initially they would start building faster horses, but they would learn pretty quickly, as Apple learned, what would be a better course of action.

Indeed. The collaborative approach of Tau is not only that people put in requirements and combine them together. It is also about creating a setting for discussion, with people discussing what software should do.

One of my old definitions of Tau, which is still relevant, is that Tau is a discussion about Tau. On Tau, people discuss what Tau should be like, and Tau becomes the consensus of the discussion.

In a social setting, people discuss what they want to happen, and then the system builds what we call an opinion map: a mapping of all the opinions in the discussion, including which opinions contradict which others. The consensus of the discussion becomes the software update.

Even what it means to be consensus is definable. That is the law of changing the laws.

Do you think there would be a learning curve for users of the system to define requirements using this logical language?

Yes, definitely. At the beginning, you will have to learn the language. It is not such a complicated language; it is quite minimalistic. But just because you control a language does not mean it is easy. Many programmers control a particular programming language, and it is still very hard to build software.

Studying the language is the easy part. There will be a learning curve, and we will try to make it easier over time by using so-called controlled natural language and better interactive tools that help you express yourself. This will be an ongoing effort.

It’s interesting what you said about language. You’re almost saying that domain understanding is harder than the syntax or the technical understanding of writing in the Tau language.

Just because I speak a little English doesn’t mean I’m Shakespeare.

Do you think there might be failure modes? Are you worried about the system becoming stuck because people initially thought something would be a good idea, and then it transpired that something else would be a good idea—but now, because of the way the system is designed, we can’t change it?

Tau is all about change. It is designed to change.

You can change it in a way that prevents other changes; there is nothing to do against that. If I give you the power to change, then you also have the power to avoid change. By the way, you also have the power to never avoid change. You can do that as well.

I’m thinking about how some religions had error correction built into them, which meant that they stayed the same and didn’t really change for millennia. Other religions were much more dynamic, splintering and mutating all over the place.

Do you think it’s a bit of a lottery? Depending on the trajectory of change, the system might become quite sclerotic, whereas if the chips fell slightly differently, it might have a very different outcome.

Suppose a new country is formed and starts with democracy. I ask you what the laws of this country will be in 20, 50, or 100 years. No one knows.

What if people said, “We need to have some kind of veto”? What if the system became so entrenched that it no longer served the desires of the users, but it had become locked in because of previous decisions?

It can happen. But logical AI helps people have guarantees about what can and cannot happen. They also have a monetary incentive to keep the system. It is a collective effort; it is not just the mistake of 1 person.

This is the risk you should accept when you want things to change, but the risk is mitigated by all these things.

It’s quite interesting. In democratic capitalism, Noam Chomsky famously said in Manufacturing Consent that we have uninformed consumers making irrational purchasing decisions. In Tau, you can say that we eliminate the deception and that people can actually see why things are happening in a certain way.

I suppose the main philosophy is that users know what’s best for them. There are people who say we need experts and need to protect people from themselves. What do you think?

I would guess that many users will delegate their voice, quote unquote. There is no voting in Tau and no need for voting, but they may delegate their voice to experts they trust. Maybe Tau will end up as a form of meritocracy.

Given the learning curve, do you think we might use something like language models, syntactic sugar, or some other way to make it easier for people to program rules into the system?

Yes. One consideration we have is to use LLMs to translate from natural language to the Tau language. We are not working on it right now, but that is definitely something on our list.

What do you think governments will think about this? Do you think they might try to subvert a system that is so democratic that the users are in control?

I don’t know.

Is that something that concerns you?

No, no. There is nothing too scary in this system. It is a blockchain controlled by its users. Why should it worry anyone?

What would be the existential threat to such a system? How is it protected from interference by other actors?

It will be deployed. It is not protected from interference by other actors, but the users will have to set the rules.

We will start with a testnet, not a mainnet. We will start with a blockchain with fake coins, where the users set the rules. Because it is only a testnet, there is no harm in restarting it. We will let the users play with the rules and, over time, come up with an initial rule set.

If they reach a deadlock, we can just push a button and restart it from scratch. This will be a very useful sandbox for the users to decide what the governance should be like. Then it can be implemented over the mainnet.

Do you agree that the philosophy of the system is that there is currently a power asymmetry? There are people who take away our agency, where agency means the ability to control the future. A system like this is emancipating in the sense that it gives users more agency.

But usually, when people get too much power and agency, other people want to take it away again.

For 1 thing, it can be a choice of users to give up their agency. For another, there is a whole other dimension to all of this, which I guess is much bigger: how programs are collectively defined and updated.

You can do it, of course, in traditional coding, but it is like the Stone Age. It is very limited and very difficult. When you just say what you want to say and it automatically becomes a computational reality, that is a different level.

You’re talking to people who know nothing about blockchain. Why should they be interested in it?

It is the future of the economy. Think about how the traditional economy works, with paper money, printing money, interest rates, politics, and all the dirty stuff. It is crazy.

Help us understand more about that. Let’s say we have the Bank of England. It sets the interest rates, it can print new money through quantitative easing, and there are all of these different levers and actions going on. We have no control over them.

You’re saying that the blockchain is a new type of financialization where there is more transparency and we understand how it works better.

That is 1 aspect of it.

What other aspects are there?

Take automation. If you want some automatic process and go to your bank app, what automatic financial processes can you do? Very few.

On a blockchain, you can do virtually anything.

You mean having custom software that runs on the blockchain and does things that you want it to do?

Yes. When someone sends me money, I might want to automatically move it somewhere. I might want to run a logic program, and depending on the output of the program, notify someone or do something.

You might want to write a program that pays your taxes automatically. It does the whole accounting and calculation, calculates how much needs to be transferred to the tax authority, and does it automatically.

Why aren’t we there? It’s 2025.

I can attest to that. Just getting my accountant access to my VAT system in the UK required an incredible amount of paperwork. I had to get him validated, they had to send him an email, and he had to send a special code back. Paying my tax is incredibly difficult.

They tried to set up a direct debit, it didn’t work, it bounced, they fined me, and I had to appeal the fine. It’s a nightmare.

You’re saying that with this structured interface, I could plug my accountant in there, pay my taxes automatically, and the whole thing would just run. We could almost have a marketplace of accountants: I don’t like this accountant, so I plug in another one, and it just works.

You don’t need accountants at all if everything is automatic.

It is easy to see that the system is in the Stone Age. As you described, in 2025 you expect everything to be automatic, instant, and accurate, but it is not like that. The monetary system is 1 of many things in life that is a century behind, if not 2 centuries behind.

There is so much room for advancement, and that is another reason blockchain is interesting.

Isn’t this one of those things where we could automate it, but weirdly we don’t? In large corporations, there are advisory committees and gating systems. You can’t check code in without release control.

My bank phones me every time I pay my staff. They block the transaction and ask who this person is, whether they sent me an invoice, and whether I know them. It’s the same conversation every time.

Maybe they’re worried that if we automated the system, it would spiral into chaos and there would be lots of fraud. Is that why they’ve put all these manual checks in?

I don’t know. But as you said before, when you asked whether user control of the blockchain would spiral into deadlocks and problems, that is exactly what happens in real legal life.

There are so many laws. How many new laws pass every year, and how many old laws are deleted every year? That is already happening in a system without logical AI—a system that does not care about your opinion.

In a way, what you’re arguing against is bureaucracy. There are so many processes in the business world where you get gatekeepers. Are you saying that a big part of this is simply that it creates jobs for people, and people like to interfere?

The only thing I advocate against is illogicalism. I’m saying, don’t be illogical.

You find illogicalism in LLMs, in social structures, and everywhere. To bring logic to life, we can mechanize it with computers. We can fix a large part of it.

Amazing. Ohad, thank you so much for joining us today. It’s been an honor.

Thank you, Tim. It’s my honor and pleasure.