Tau Language - studying the source code (Aug 2 2024)

Tau Language Github code analysis

Tau Language seems to be in the final stages of development before the alpha release. I know this because I can see on the Github. So let's discuss what has happened. Over a week ago David created a spec for the solver. A solver is a piece of software which can solve a mathematical problem, and typically it does this by a sort of search process. In the cause of Tau Language the solver David is implementing is a minterm solver which can be used to solve logic formulas which are processed into the minterm form.

Logic formulas in Tau Language go through different manipulations to get into the form which is easier for the computer to work with. This is called normalization, and it simplifies the data basically. There are a bunch of different normal forms, which can be for different reasons which I won't dive into, but in general Tau Language works with boolean formulas, and what we want is for the user to be able to enter their formulas, and have it be computable and executable.

A formula in Tau Language for example can be a specification of an application. Tau Language needs to have the ability to take this formula of a specification and using it's algorithms turn it into executable software. The key steps in this process is satisfiability, and also the solver (the minterm solver). Splitters play a role in allowing this to happen as well, allowing for the algorithms to work.

David recently added testing for the minterm solver, and he also improved the efficiency of the iterator. The testing is going to help with debugging. There also is an execution API, and my best guess is this part of how a formula becomes software. As long as the computer knows what to do at every step, it can generate and run the software, from the specification formula.

I estimate it's close because:

1. Lucca recently implemented splitters. This allows for the implementation of the algorithms in TABA.
2. David recently implemented a solver. A solver is a key component of model checking, of self optimization, of AI.
3. David implemented some testing infrastructure for the solver and even some optimizing features.
4. All that hasn't been done, is outlined clearly in the comments, so readers with a C++ background can see what needs to be done, including the references to algorithms from TABA, including the priority level high or low, including ideas, including potential optimizations.
5. The hardest parts are over. Hardest meaning the most novel to implement stuff out of TABA. Splitters for example are entirely novel, and some of the formulas seem to be invented by Ohad or reference arcane books which no one but Ohad has access to, but as long as these work, and the theory is sound, it's implementable and computationally feasible.

So I would say it's 98 to 99% complete.

What will we want to see in the coming days and weeks? We will want to see an announcement from David and Lucca of some sort that shows an input formula becoming an execution of software. Once we see this, in my opinion it's the ultimate demo, ultimate proof of concept, where you will see that you can input a specification and get bug free software as output.