ANTHILL: a progressive formalization language for agent-supported software projects

The article presents the Anthill language — a specialized language for progressive (gradual) knowledge for malization, designed for use in real-world software projects with the integration of agent support, in particular large language models. Anthill allows you to describe, accumulate and maintain...

Повний опис

Збережено в:
Бібліографічні деталі
Дата:2026
Автори: Shevchenko, R.S., Doroshenko, A.Yu., Yatsenko, O.A.
Формат: Стаття
Мова:Українська
Опубліковано: PROBLEMS IN PROGRAMMING 2026
Теми:
Онлайн доступ:https://pp.isofts.kiev.ua/index.php/ojs1/article/view/887
Теги: Додати тег
Немає тегів, Будьте першим, хто поставить тег для цього запису!
Назва журналу:Problems in programming
Завантажити файл: Pdf

Репозитарії

Problems in programming
Опис
Резюме:The article presents the Anthill language — a specialized language for progressive (gradual) knowledge for malization, designed for use in real-world software projects with the integration of agent support, in particular large language models. Anthill allows you to describe, accumulate and maintain domain knowledge, functional and non-functional requirements, design solutions, invariants, integrity constraints and property proofs in a single structured knowledge base. A distinctive feature is that the knowledge base is stored directly in the pro ject repository file system, which ensures close versioned synchronization of specifications with code and fa cilitates their evolution throughout the development life cycle. The core of the language is made minimal and consists of only four basic constructs: namespace, sort, rule and operation. This architecture is similar to the core of modern automated theorem proving systems (e. g. Lean, Coq), where a small trusted core performs on ly the correctness check of the derivation, while the search for proofs, rule generation, specification refinement, and resolution of commitments are delegated to external agents. The main innovation of Anthill is the built-in support for partial (progressive) formalization: one and the same language allows for the description of knowledge across the entire spectrum — from free-text natural language comments in blocks through semi formal machine-verifying rules (Horn clauses) to fully formal proofs and laws of algebra. Three application examples are considered: structured task management, specification of communication protocols for embedded systems, and proof of properties at the compilation stage.Problems in programming 2026; 1: 4-13