HVM і Interaction Calculus: надійна основа для AI-коду

Що саме будує Віктор Таелін

Для мене головний сенс HVM не в черговій незвичній мові, а в спробі дати згенерованому коду малу й сувору обчислювальну основу. У статті про HVM2 систему описано як паралельний обчислювач для розширених interaction combinators із виконанням на CPU та CUDA/GPU.

Станом на обговорення у вересні 2026 року я ще не тестував цю зв'язку на практиці, тому не буду вдавати, що маю готовий вердикт. Але за роботою Віктора Таеліна я стежу давно: тут видно послідовну інженерну лінію, а не раптовий проєкт, зібраний навколо модного терміна.

В основі лежить Interaction Calculus — компактна мова термів, близька за духом до лямбда-числення. Обчислення виражається через невеликий набір вузлів і локальних правил взаємодії, що відкриває шлях до паралельної редукції графа.

У статті HVM2 заявлено майже ідеальне прискорення зі збільшенням кількості ядер для програм без послідовних обмежень. Окрема реалізація для CUDA, згідно з роботою про lock-free evaluator, редукувала великі графи на GPU з тисячами одночасно активних потоків. Це твердження авторів і результати публікацій, а не мої вимірювання.

У матеріалах HVM4 описано наступний крок: компіляція функцій Interaction Calculus, зокрема суперпозицій, безпосередньо в машинний код без накладних витрат. Якщо цей шлях буде стійким на реальних програмах, проміжна модель перестане бути гарною теорією та стане повноцінним runtime.

Порівняння з Lean тут корисне лише як груба аналогія. Ідея не в тому, щоб попросити модель не помилятися, а в тому, щоб обмежити результат формальною системою, де виконання визначається точними правилами. Водночас HVM передусім налаштований на обчислення коду, а не на математичні доведення.

Чому це цікавіше за звичайний промптинг

Суворий runtime може підвищити надійність AI-кодингу сильніше, ніж чергова інструкція в системному промпті. Модель і далі здатна породити хибну програму, зате між генерацією та виконанням з'являється компактний шар з однозначною семантикою.

Практичний виграш можливий одразу в кількох місцях: перевірюване зниження коду до малого ядра, явна робота з дублюванням і суперпозиціями, паралельне виконання без прив'язки лише до CPU. Особливо цікаво це для агентів, які мають не просто написати текст програми, а безпечно виконати й перетворити його.

Проблем я очікую в зручності компіляції звичайного коду в цю модель, налагодженні, передбачуваності споживання ресурсів і розриві між ефектними паралельними прикладами та щоденними послідовними завданнями. HVM виглядає не заміною здоровому глузду моделі, а способом зробити її помилки локальнішими та помітнішими. Саме на переході від красивої редукції до буденної експлуатації й вирішиться доля ідеї.

Раніше ми розбирали компілятор Claude: що він здатен зібрати та де його підхід ламається на завданнях системного програмування. Цей огляд добре підкреслює ідею Lean-компілятора, де коректність будується через код і формальні перевірки.