🛠 Última actualización de desarrollo de julio: construyendo el núcleo de la alfa TestNet de Tau Net El equipo avanzó aún más hacia TestNet Alpha al finalizar la creación de bloques, mejorar el rendimiento del análisis y desarrollar nuevos algoritmos para la normalización de fórmulas. Resúmenes: - TestNet Alpha: Creación de bloques, vinculación y almacenamiento raíz de Merkle completados - SAT Solver: La migración de Z3 a CVC5 desbloqueó una mejor normalización y satisfacibilidad - Motor de análisis sintáctico: 60% de aumento del rendimiento + posible nueva patente de análisis sintáctico - Investigación y desarrollo de lenguajes: Normalización anti-prenexing y lista para la eliminación de cuantificadores booleanos. Ohad ha estado revisando los últimos documentos de lógica temporal. Tau Net y $AGRS se mantienen muy por delante del progreso académico actual en el campo. Marcas de tiempo: 00:12 - Extracto de Karim 03:48 - David (Desarrollador principal) - Se cambió con éxito de Z3 a CVC5, lo que mejoró el rendimiento general del solucionador. - Trabajo completado en módulos de normalización, satisfacibilidad e intérprete con CVC5. - Se implementó el enfoque sugerido por Ohad de diferir la resolución literal para ecuaciones de vectores de bits. - Ayudó a Umar con revisiones de código y depuración. 05:36 - Lucca (Desarrollador del lenguaje Tau) - Desarrollé la especificación inicial para un algoritmo para eliminar cuantificadores de funciones para su uso en la función de tabla de Tau. - Se integró en el algoritmo de normalización anti-prenexing para manejar fórmulas no cubiertas por CVC5. - Preparándose para implementar este algoritmo ahora que el pseudocódigo está finalizado. - Comenzó a usar la implementación del nuevo árbol de Tomáš y ayudó a resolver sus problemas finales. 08:30 - Andrei Korotkoff (Desarrollador Senior) - Se completó el hito alfa de la red de prueba para la producción y el almacenamiento de bloques, incluido el manejo de mempool, la vinculación de bloques, el cálculo de la raíz de Merkle y la persistencia de la base de datos. - Este trabajo sienta las bases para el siguiente hito: el estado persistente de la cadena basado en el historial de bloques. - Desarrollé una herramienta compleja de pruebas de carga para simular el comportamiento del intérprete de Tau y la dinámica de la cadena de bloques bajo revisión puntual. 11:20 - Tomáš Klapka (Desarrollador Senior) - Se corrigieron varios problemas del interruptor de árbol, incluido el manejo de negaciones, errores tipográficos gramaticales y errores de inferencia de tipos. - Se ha refactorizado la biblioteca del analizador para que sea solo de encabezado. - Se creó soporte para Docker y versiones nocturnas para la herramienta TGF y el analizador. - Se actualizó el lenguaje Tau para integrar el analizador mejorado. 12:26 - Ohad (Fundador y CTO) - Centrado en el diseño de nuevos algoritmos y la colaboración en equipo. - Exploré lenguajes independientes del dominio para mejorar los procedimientos de decisión. - Revisó artículos académicos recientes sobre lógica temporal y confirmó que Tau se mantiene a la vanguardia de la investigación actual.