Данные свидетельствуют о том, что самая большая проблема, с которой сталкиваются модели, — это не синтаксис. Это согласованность, а не масштабируемость. Модели испытывают трудности с поддержанием инвариантов в кодовой базе, пониманием волновых эффектов изменений и рассуждениями о состоянии во времени. Они — сопоставители шаблонов, оптимизирующие локальную правдоподобность, а не архитекторы, учитывающие всю систему. Поэтому создание языка для них означает решение этой проблемы. Каждое проектное решение в Vera призвано быть ответом.
Vera отдает предпочтение проверяемости, а не корректности. В дизайне делается акцент на коде, который можно механически проверить, и при возникновении ошибки компилятор предоставляет объяснение на естественном языке с конкретным решением. Он не дает модели непрозрачный отчет о состоянии, а передает инструкции по его исправлению.
Традиционные компиляторы создают диагностические сообщения для людей. Вместо этого Vera генерирует инструкции для модели, написавшей код. Что пошло не так, почему, как это исправить с помощью конкретного примера кода и ссылки на спецификацию. Таким образом, выходные данные компилятора предназначены для прямой передачи модели в качестве контекста для исправления.
Это важно, потому что естественный рабочий процесс генерации кода для ИИ — это цикл: написание кода, проверка, исправление, повторение. Если на этапе проверки выдаются результаты, на которые модель не может отреагировать, цикл прерывается. Диагностика Vera замыкает этот цикл.
Vera отдает предпочтение явности, а не удобству. Все изменения состояния объявлены, все эффекты типизированы, все контракты функций являются обязательными. Нет неявного поведения. Контракты являются источником истины: каждая функция объявляет, что она требует, что она гарантирует и какие эффекты она выполняет. Даже однострочный код имеет полный контракт. Компилятор затем проверяет его статически, где это возможно. - отсюда
