Show HN: Lean4 Datalog DSL Based on Google Zanzibar for AI Projects
ZIL est un petit langage relationnel qui décrit des objets nommés, les relations entre eux et des règles Horn pour dériver des relations supplémentaires, et il est implémenté dans Lean 4. Il s'inspire du modèle de tuples de Zanzibar pour représenter des faits relationnels compacts et permet d'exprimer des patrons d'autorisation et d'héritage de membres de groupe. Dans Lean, ZIL enregistre faits, schémas, règles et preuves certificatives pour relier déclarations, exigences, tests, documents et tâches au sein d'un dépôt. Le moteur applique des règles de style Datalog pour inférer relations telles que la couverture d'exigences et l'impact des changements, en conservant des explications et des niveaux de confiance (asserted, graphDerived, certified). L'écosystème inclut des outils persistants et échangeables (exécutable natif, snapshots ZILX/ZILD, export Soufflé/Prolog, exemples et linting) pour intégrer développeurs, CI, documentation et assistants IA.