Karim: Here is an overview of the development progress that we’ve done so far this year. So, as you all know our development has been going through two major tracks. The first one is on the Agoras Live web application which is essentially a nucleus for the Tau system. And of course, also TML, the Tau Meta-Language, which is at the core of Tau. We will be using it both for translations between languages but also as the main core technology for our logical solvers.
The Agoras Live application has been fully developed and modules from testing will be ready for deployment early next year. In the past year, we’ve gone through several graphical redesigns of the interface itself based on initial feedback we got from some users. We’ve added a web wallet for crypto payments and authentication through the web wallet; that’s how you’ll login to Agoras Live. We’ve added the concept of public sessions where teachers basically can hold open sessions that anybody can join. We’ve added a lot of call management features including “my session” feature for teachers and students to manage their history of sessions but also calendar functions for future sessions. We’ve also added peer-to-peer reviews between all the users of Agoras Live, both teachers and students. And then that was it in terms of functionality towards the end of the year. We started looking at the overall architecture of the application with an eye towards deployment DevOps and scalability and we’ve actually ended up refactoring the entire back end, and in the process also fully documenting the back end in order to make it easier in the future to maybe even reimplement the front end. Hopefully, sometime early next year after we’ve done our testing, we should be able to release version 1.0.
On the TML side, I think we’ve accomplished all the features that Ohad had set out for us at the beginning of the year. We have a TML 1.0 version ready to release and test for you guys, actually it’s been available for a while on what we call the TML IDE. That Tomas had laboriously developed. So, the TML IDE essentially is a web-based tool that you guys can use to look at several examples of TML programs that you can edit, play with and look at the output. Tomas added a lot of improvements to that including syntax highlighting. We’ve also had highlighting of TML in VS code or Vim, if that’s your favorite editor of choice. So, you can write TML and VS code if you want to. We’ve also added a lot of built-ins into the TML language itself, except built-ins that are essentially external functions that you can call in TML. So, it could be things like printing or any advanced arithmetic functions that you wanted to do. We’ve also extended the TML syntax to allow for multiple ins into one rule but also, we’ve added cashing for the built-ins. There’s also now an API to implement your own built-ins if you want to roll up your sleeves and do that. We tried our hand at solving at least one practical problem in TML which is well or at least a well-known problem which is the puzzle game called Sudoku. So, Tomas implemented that in TML actually and using several approaches and we learned some very good lessons on both in terms of TML performance but also, we added a new thing called state blocks which helps with the control flow of TML.
We’ve continued to push the capability of that IDE built into a web browser. I mean it’s very capable. It does almost everything that you can do on the command line. We’re working on the persistence of TML programs which has something to do in the future with what we call the BDD network and the ability to store and retrieve and cache logic computations. So, that’s also a very important line of work.
On the logic portion Juan extended the first order logic functionality of TML, but he also worked on a second order logic.
Not necessarily a complete solution but a first version of second order logic that is very useful in some cases. Juan also extended the arithmetic operators. He actually reimplemented them just to enhance performance and experimented with several approaches of all second order logic. What you guys know is a very hard problem. Juan started out the year by migrating AGRS from the Omni layer to being an Ethereum ERC 20 token, which allowed us to list AGRS on several crypto exchanges.
Umar has done a lot of work on extending the syntax of the TML. Now we can specify the syntax in EBNF, so that improves the parsing performance. He also added regular expressions and macros to TML. A major improvement was conversion of the universe of size two, which is kind of an internal optimization but it’s a very important one. He also added specific types at the TML so you can specify the exact number of bits per variable which helped a lot with performance. He also added type checking and type inferences, which has made the TML a much more robust programming language. We continue to push the envelope on the capabilities of TML.
We already started working on what’s called an early parser, which is a very powerful parser engine. We think we’re ready to release a version next year, but we continue to work on TML as our core technology for Tau.
Juan: I did work on the logic capabilities of our system. So, I fixed several parts to the first order logic feature with the support of the other team members, particularly Tomas, Lucca and Murisi. All of them found issues in implementation, so where I address those functional bugs. I also extended, in particular, the first order logic with the uniqueness qualifier, which is running for computing on the BDD layer. So, it’s a built-in or slash primitive handler.
With regard to the arithmetic capabilities, I did an implementation of our count handler or built in, plus I redesigned all the BDD edition, which is operating directly on the BDD data structure. For which we are expected to have relevant performance gates. In the short term, we will be testing those new capabilities and also the less or equal built in, which is also running directly on BDD data structure, which is compatible with what is the new bit universe transformed programs that Umar put together during this year.
There is a lot of possible work to be done on arithmetic. We have some work remaining on the logarithmic function and there are many possibilities to extend the system with regards to its arithmetic abilities. It’s likely that we may want to focus also on some primitives or handlers. We need to relate it to be a blockchain, let’s say like crypto primitives networking and also some shared memory or global memory synchronisation and access between the nodes of the system. So, there are some relevant decisions to be made. We are working on them. It’s likely that built-ins, as the concept of the built-ins may grow in different directions. Say arithmetic or the other primitives that I mentioned related to be a blockchain or a distributed system. Finally, I did participate during the whole year in the Tau academic panel sessions, which of course was a very intellectually demanding task just by listening to what was being done there. I’m looking forward to and especially putting the attention on what are the automaton related aspects of the system. And also, related to a hypothetical machine that may have to address some problems related to the system.
So, there is very interesting theoretical computer science work that has been done there, of course as well as logical and mathematics really. I’m enjoying what is being done with the professors that are assisting us with Ohad’s lead there. We’re exploring new horizons and really the state of the art in computer science I would say. We are trying to tackle a very hard problem and we will continue improving the solution that we are figuring out.
Lucca: This month I continued studying the theory of algebraic effects, which I started last month. I also looked into how Monarch Haskell exactly worked and what the use cases are. I did that in order to better understand, let’s say the general theory of side effects better in order to contribute ideas on how we can enable side effecting programs in our language we are developing. This is ongoing work and discussion within the academic panel.
I have continued the development of the two CNF extraction feature. I further enhanced the shared universe for the two CNF formulas. That in particular meant the implementation of a canonically persistent shared data structure which can hold implications, so basically elements which have a first and a second component. I’m looking forward to a new year. I’m very excited to work on and following the challenges that we encounter.
Tomas: My accomplishments in the year 2021. First, it’s the TML online editor, which is available at TML.idni.org. Where anyone can try TML online on the web without installing or combining anything. It also contains a lot of examples of various TML features. Next was TML syntax highlighting for the online editor and also made syntax highlighting extensions for VS code and Vim editors. Regarding TML itself, I’ve reworked built-in support, so devs have a better API for defining new built-ins. Variables that are groundless when used in built-ins. TML programmers can use multiple built-ins per rule. They can control cache of built-in results to control how often is every built in cold. And I’ve added various built-ins for printing to output streams of TML. Then I was trying to write some more complex programs in TML, namely Sudoku solvers. From this endeavour, I came to a conclusion that TML needs a new syntax construct to make complex TML programs more readable. I’ve implemented a new structure called state blocks. I’ve also continued to maintain JavaScript build of TML by using Emscripten. And finally, this month I’ve been researching the usability of a boost inter process library for persistence of TML.
Andrei:This last month, I was publishing the code. I was writing some more documentation that we needed and I was making sure that for example a tester can run backend queries right inside Swagger, and we are looking forward to a tester report to finish building of this basic Agoras Live platform and release it pretty soon enough.
Umar: The good thing is that, in this month we have made a significant contribution in terms of turning the recognizer into a parser. Previously, for any given sentence an earlier recognizer could only say yes or no, whether the sentence matches the grammar or not or part of the language of the grammar or not. But now with adding that parsing capabilities, we can not only see the syntactic structure of how a given sentence is derived, but we are also able to encode or represent and store that syntactic structure compactly in a graph. That’s crucial, because there are many cases where for a given context free grammar with ambiguity, you can have an exponential number of individual parse trees. That would be very cost prohibitive in terms of storage. So, one of the things that we spend time in this month is how to have the right data structure to store the parse forest. Having done so, we have tested it with different grammars from the literature, from the research papers, because that’s where some of the tricky test cases were presented. Now in the process of fine tuning it, optimising it and making sure it becomes more efficient.
Also, we are in the process of trying to complete an end-to-end workflow here, that given any input sentence and a given grammar, how we can construct a parse free. Then turn that parse tree into TML facts. This is so that TML programs can use those facts to make changes, process them, transform or translate them into other syntax structures.
Ohad: I continue to enhance our logical framework to be able to specify programs. Because after all Tau is a program and it’s all about the users controlling this program. Being able to specify by means of consensus. It is not a difficult task. There are many formalisms in the literature of how to represent programs in logic but they don’t answer our basic requirements, the requirement of being purely logical. So, it makes sense to specify programs by means of consensus, which is what we want. Most of the specification languages out there don’t have that thing. It is meaningless to speak about consensus in those languages.
The other difficulty is that even if we are able to specify programs in pure logic and have meaningful consensus, this logical framework should fit the ideological framework of ability to speak about truth inside the language. So, this month and also in the next month and the big effort in specifying programs under this framework is continued.
