Перша формальна система визначає формальний підхід до математичної верифікації та описує спробу автора у цій парадигмі побудувати замкнену уніфіковану систему формальних мов для програмування, математики та філософії. В процесі розробки моделі такої системи автору довелося апробувати частини її імплементації для головних SML-подібних формальних академічних мов, мови Erlang та інших (загалом 7 мов). За 10 років автором було проаналізовані синтаксис та семантика основних мов програмування (більше 50 мов) з різних промислових та академічних доменів, 8 мов з яких були особисто реалізовані автором. В роботі описані 8 мов уніфікованої мовної системи (концептуальна модель) та представлені 2 їх імплементації.

Головним чином, натхнення було почерпнуте з LISP-машин минулого, APL-систем, перших систем доведення теорем таких як AUTOMATH, віртуальних маших паралельної та узгодженої обробки нескінченних процесів, таких як BEAM, та кубічних MLTT-пруверів.

Суть роботи полягає в побудові унікальної замкненої си- стеми яка складається з: 1) системного програмного забезпечення – модального середовища виконання разом з інтерпретатором написаним на формальній мові; 2) бібліотека та архітектура прикладного програмування N2O.TECH для середовищ виконання; 3) прикладного програмного забезпечення — системи вищих формальних мов, для яких надано моделі, імплементації; 4) базова бібліотека разом з математичними компонентами (програми на вищих мовах).

Синтансичне дерево мови інтерпретатора містить модуль лінивих відкладених обчислень (CPS), та розширення синтаксичного дерева спеціальними командами пов’язаними з середовищем виконання (управління процесами виконання). Програми таких інтерпретаторів виконуються у певній пам’яті, яка використовується як контекст виконання. Кожна така програма виконується як атомарний поток інструкцій на одному ядрі фізичного процесора. Ситема віртуальних процесів містить SMP/AMP планувальник, який управлє CPS-програмами які виконують інтерпретатори на кожному з фізичних ядер процесора.

Мотивація для побудови інтерпретатору, який повністю розміщується разом з программою в L1 кеші (який лімітований 64КБ-256КБ) базується на успіху таких віртуальних машин як LuaJIT, V8, HotSpot, а також векторних мов програмування типу К та J. Якби ми могли побудувати дійсно швидкий інтерпретатор який би виконував програми цілком в L1 кеші, байткод та стріми якого були би вирівняні по словам архітектури, а для векторних обчислень застосовувалися би AVX інструкції, які, як відомо перемагають по ціні-якості GPU обчислення, то такий інтерпретатор міг би, навіть без спеціалізованої JIT компіляції, скласти конкуренцію сучасним промисловим інтерпретаторам, таким як Erlang, Python, K, LuaJIT. Для дослідження цієї гіпотези мною було побудовано експериментальний інтерпретатор без байт-коду, але з вирівняним по словам архітерктури стрімом команд, які є безпосередньою машинною презентацією конструкторів індуктивних типів (enum) мови Rust.

Ключовим викликом тут стали лінійні типи мови Rust, які не дозволяють звертатися до посилань, які вже були оброблені, а це впливає на всю архітектуру тензорного преставлення змінних в мові інтерпретатор CPS, яка наслідує певним чином мову К.

Середовище виконання мість базову бібліотеку формалізовану в PureScript, а також серію експериментів N2O.DEV, повні версіх яких доступні для мови Erlang, Elixir та Hamler.

Тут йдеться про мови програмування придатні для доведення теорем, та їх таксономію від найелементарніших (чистої системи з одним типом Π) до найпотужніших гомотопічних систем. Одна така гомотопічна система є кінцевим завданням цього розділу — побудова моделі гомотопічного верифікатора. В процесі його побудови в цьому розділі ми розглянемо під мікроскопом складові частини його нижчих мовних рівнів. Застосуємо категорну семантику для мов програмування і будемо розглядати мови програмування як моноїдальні мовні категорі, об’єкти яких є просторами усіх програм цих мов програмування, а морфізми — правила верифікації та компіляції цих програм. Мови розкладаються у спектральну (індексовану натуральними числами N → U) послідовність мов, кожен елемент якої є мовою програмування, яка не містить синтаксичне дерево вищої мови програмування.

Система вищих мов мість базові бібліотеки PURE для системи PTS та HOMOTOPY для системи MLTT/CCHM/HTS. Для побудови вищих мов використовувалися мови OCaml та Erlang.