🛠 Останнє липневе оновлення розробника – створення ядра TestNet Alpha від Tau Net Команда просунулася далі до TestNet Alpha, завершивши створення блоків, покращивши продуктивність парсингу та розробивши нові алгоритми для нормалізації формул. Підкреслює: - TestNet Alpha: створення блоків, зв'язування та кореневе сховище Merkle завершено - SAT Solver: міграція з Z3 на CVC5 відкрила кращу нормалізацію та задовільність - Parsing Engine: підвищення продуктивності на 60% + потенційний новий патент на парсинг - Мовні R&D: Нормалізація проти пренексінгу та специфікація виключення булевого квантора готова. Охад рецензував останні статті з темпоральної логіки. Tau Net і $AGRS залишаються далеко попереду поточних академічних досягнень у цій галузі. Мітки: 00:12 - Підсумок Каріма 03:48 – Девід (провідний розробник) — Успішно перейшов з Z3 на CVC5, покращивши загальну продуктивність розв'язувача. - Виконано роботу над модулями нормалізації, задовільності та інтерпретатора з CVC5. - Реалізовано запропонований Огадом підхід відкладення літеральної роздільної здатності для рівнянь бітових векторів. - Допомагав Умару з рев'ю коду та налагодженням. 05:36 - Лукка (розробник мови тау) - Розроблено початкову специфікацію алгоритму для виключення функціональних кванторів для використання у функції таблиці Тау. - Інтегровано його в алгоритм нормалізації проти пренексінгу для обробки формул, які не охоплені CVC5. - Підготовка до реалізації цього алгоритму тепер, коли псевдо-код завершено. - Почав використовувати нову реалізацію дерева Tomáš і допомагав у вирішенні його остаточних проблем. 08:30 - Андрій Короткофф (старший розробник) - Завершено етап альфа-версії тестової мережі для виробництва та зберігання блоків, включаючи обробку мемпулів, зв'язування блоків, обчислення кореня Меркла та стійкість бази даних. - Ця робота закладає основу для наступної віхи: постійного стану ланцюга на основі історії блоків. - Розроблено складний інструмент навантажувального тестування для моделювання поведінки інтерпретатора Tau та динаміки блокчейну при точковому перегляді. 11:20 - Томаш Клапка (старший розробник) — Виправлено кілька проблем із перемиканням дерева, включаючи обробку заперечень, граматичні друкарські помилки та помилки виведення типів. — Перероблено бібліотеку парсера так, щоб вона була лише заголовком. — Створено підтримку Docker та нічні релізи для інструменту та парсера TGF. — Оновлено мову Tau для інтеграції покращеного парсера. 12:26 - Охад (засновник і технічний директор) - Зосереджений на новому дизайні алгоритмів та командній співпраці. - Досліджено доменно-незалежні мови для вдосконалення процедур прийняття рішень. - Розглянуто останні наукові роботи з темпоральної логіки та підтверджено, що Тау випереджає поточні дослідження.