The post has been translated automatically. Original language: Russian
This week we completed an important change in the Sekura JS architecture: the SJV formal verification system became an independent component and is no longer part of the compiler.
At first glance, this looks like a regular refactoring. In fact, it's about the boundary of trust.
The compiler obtains the source code of the program and creates an executable object. If the same mechanism then actually confirms the correctness of its own result, the independence of the verification is conditional. An error in the general logic can equally affect the creation of a program and its verification.
Therefore, these tasks were separated.
Sekura JS is now responsible for the language and compilation. The general part parses the source text, resolves names, types, structures, and expressions. After that, the compiler creates an executable program.
SJV works separately. To test the program on our current architecture, it examines the resulting executable object, decodes machine commands, and verifies its behavior relative to a given formal specification.
That is, the question is not posed like this: "did the compiler translate this text correctly?"
The question is different: does the created program have the properties that we required of it?
This is a fundamental difference.
SJV received a separate startup interface, its own verification core, and a separate component boundary. At the same time, we did not duplicate the description of the language itself: Sekura JS parsing and its basic semantics remain common where it is really necessary.
As a result, two independent roles emerged.
Sekura JS creates a program. SJV checks its properties.
For us, this is an important step in a broader sense. Today, code is increasingly being created not only by humans, but also by artificial intelligence. The cheaper it becomes to create a program, the more important it becomes to have an independent way to verify the properties of the result.
We are not trying to prove that the author of the program is not mistaken. We are building a system in which the correctness of individual properties can be checked regardless of who wrote the code and how it was obtained.
На этой неделе мы завершили важное изменение в архитектуре Sekura JS: система формальной верификации SJV стала самостоятельным компонентом и больше не является частью компилятора.
На первый взгляд это похоже на обычный рефакторинг. На самом деле речь о границе доверия.
Компилятор получает исходный текст программы и создаёт исполняемый объект. Если затем тот же механизм фактически подтверждает правильность собственного результата, независимость проверки получается условной. Ошибка в общей логике может одинаково повлиять и на создание программы, и на её проверку.
Поэтому эти задачи были разделены.
Sekura JS теперь отвечает за язык и компиляцию. Общая часть разбирает исходный текст, разрешает имена, типы, структуры и выражения. После этого компилятор создаёт исполняемую программу.
SJV работает отдельно. Для проверки программы на нашей текущей архитектуре она рассматривает уже получившийся исполняемый объект, декодирует машинные команды и проверяет его поведение относительно заданной формальной спецификации.
То есть вопрос ставится не так: «правильно ли компилятор перевёл этот текст?»
Вопрос другой: обладает ли созданная программа теми свойствами, которые мы от неё потребовали?
Это принципиальная разница.
SJV получила отдельный интерфейс запуска, собственное ядро проверки и отдельную границу компонентов. При этом мы не стали дублировать описание самого языка: разбор Sekura JS и его базовая семантика остаются общими там, где это действительно необходимо.
В результате появились две независимые роли.
Sekura JS создаёт программу. SJV проверяет её свойства.
Для нас это важный шаг и в более широком смысле. Сегодня код всё чаще создаётся не только человеком, но и искусственным интеллектом. Чем дешевле становится создание программы, тем важнее становится независимый способ убедиться в свойствах полученного результата.
Мы не пытаемся доказать, что автор программы не ошибается. Мы строим систему, в которой правильность отдельных свойств можно проверять независимо от того, кто написал код и каким способом он был получен.
Share
