The post has been translated automatically. Original language: Russian
Sekura JS and Zig largely proceed from a similar idea: the system language should allow the developer to understand well what is happening with the program at a low level.
Both languages try not to hide working with memory behind a large runtime environment. Explicit actions, predictable program behavior, and the ability to use a language close to the hardware are important to them.
But then their goals noticeably diverge. Zig is being created as a general-purpose language for a variety of architectures and operating systems. Sekura JS is being developed as part of its own software and hardware stack, where the compilation result should be suitable for subsequent formal verification.
Why is Zig interesting for comparison
In the official description of Zig, simplicity and clarity are named as one of the basic principles of the language. There is no hidden memory allocation and hidden management transitions, and memory management remains the responsibility of the program.
This makes Zig interesting precisely in comparison with Sekura JS.
Both languages assume that it is useful for a system developer to see the cost and consequences of operations performed. If a program allocates memory, accesses a function, or performs a specific action, it is desirable that this is clear from the code itself.
This approach differs from languages where much of the work can happen automatically and remain hidden behind language constructs.
Clarity as a general property
Sekura JS also does not seek to hide the architecture of the machine.
The language has explicit work with memory, pointers, arrays, and structures. Signed and unsigned integer types of 8, 16, and 32 bits are used.
The programmer works with a model close to the Memora8 architecture. The location of the data and the machine representation matter and are part of the language structure.
Therefore, at the level of general philosophy, there are indeed similarities between Sekura JS and Zig: the fewer unexpected hidden behaviors, the easier it is to understand the program.
The difference starts with the platform
Zig is a general purpose language. Its development tools are focused on a large number of hardware platforms and allow you to build programs for various target systems.
Sekura JS is created differently.
Its main target architecture is Memora8. The language, compiler, and processor model are developed as related parts of a single system.
This deliberately reduces versatility.
Instead, it becomes possible to determine in advance the computational model, the size of values, the rules for working with memory, and the relationship between language operations and machine instructions.
For Sekura JS, such certainty is needed primarily for formal verification.
Working with memory
Zig does not perform memory management for the programmer. Functions and data structures that require dynamic memory receive an explicit memory allocation facility. This approach allows the language to be used in environments where there is no conventional operating system.
Sekura JS also uses explicit memory, but the language structure is even more closely related to the Memora8 machine model.
A pointer represents an address in a 32-bit space. When working with arrays, the size of the element is taken into account, and when accessing structures, the placement of its fields is taken into account.
That is, in both languages, the developer has low-level control, but this control is used in different architectural environments.
The Zig should remain suitable for multiple systems. Sekura JS can rely on a pre-defined platform.
What happens after compilation
This is where the main difference comes in.
For Zig, the result of the compiler is a program or library for the selected platform. Further, the quality of the program is ensured by the usual engineering means: testing, runtime checks, code analysis, and other methods.
In Sekura JS, the machine result of compilation is also considered as an object of formal verification.
The source program is converted to SOBJ, a machine object for Memora8. The formal SJV requirement is set separately.
After that, it is checked whether the actual behavior of the machine code corresponds to the specified property.
Thus, compilation in Sekura JS is not necessarily the last step before executing the program.
After that, an evidentiary check can begin.
Why is the machine object being checked?
You can check the properties of the source code of the program, but there is a compiler between the source code and the processor.
If the compiler made a mistake when selecting instructions, placing data, or performing optimization, the correctness of the source text alone does not guarantee the correctness of the machine result.
Therefore, the received SOBJ is checked in Sekura JS.
SJV uses the formal requirement and the Memora8 instruction model to investigate the behavior of machine code.
If there is a condition that violates a given property, the check should detect it. If a violation is not possible in the specified area, the property receives a formal confirmation.
Simplicity of language is needed not only by man
In Zig, clarity helps the developer understand the program and its cost. The official description of the language explicitly emphasizes the lack of hidden flow control and hidden memory allocation.
In Sekura JS, simplicity has another purpose.
The program should be understood not only by a person, but also by a means of formal verification.
The fewer possible interpretations a language construct has, the easier it is to link it to machine code and then to a mathematical model.
Therefore, the limitations of Sekura JS are seen not only as a way to make the language simpler. This is part of the overall task of building a testable stack.
Modules and boundaries of the system
Sekura JS is built around an explicit modular model.
One source file describes one module. A machine object, information about data placement, and a description of the available interface can be generated for it.
Such a device helps to define the boundaries between the parts of the system.
This is especially important for formal verification. You can link a requirement not to the entire program at once, but to a specific module and a specific result of its compilation.
Zig also allows you to build large modular programs, but its organization is not determined by the task of creating an evidence chain for a specific hardware architecture.
Optimizing and preserving behavior
Both languages have a compiler that can transform a program to produce more suitable machine code.
In Sekura JS, we are interested in an additional question: has the formally defined property been preserved after these transformations?
Therefore, the same source program can be compiled with different levels of optimization, and each resulting machine object is tested against the same requirement.
This way, the optimizer does not become a fully trusted part of the chain.
Its result can be checked separately.
Why not just use Zig
If the task is to develop common system software for existing architectures, Zig offers significantly more extensive features and ready support for multiple platforms. On the official website, it is explicitly positioned as a general-purpose language and a set of tools for creating reliable and portable software.
Sekura JS solves a more narrow task.
It is created simultaneously with Memora8, the Reganta system software and formal verification tools.
Therefore, it is not required to be a universal language for all existing platforms.
What is required is to maintain a fairly simple and definite relationship between the source program, the machine code, and the formal property.
Two variants of the explicit system language
Sekura JS and Zig show that the idea of a simple and explicit system language can be used for different purposes.
In Zig, explicitness helps to create portable low-level software without hidden memory and execution flow management. At the same time, the language remains designed for a wide range of architectures and tasks.
Sekura JS uses a similar principle of explicitness, but within a much narrower system.
His task is not only to create understandable machine code, but also to link this code to a formal requirement and verify it relative to the Memora8 processor model.
Therefore, the main difference can be formulated simply.
Zig aims to provide an explicit and universal system programming tool. Sekura JS uses explicitness as the basis for building a software layer of a formally verifiable stack.
It is this goal that defines the Sekura JS device and explains why the language deliberately remains closely linked to its own hardware platform.
Sekura JS и Zig во многом исходят из похожей идеи: системный язык должен позволять разработчику хорошо понимать, что происходит с программой на низком уровне.
Оба языка стараются не прятать работу с памятью за большой средой исполнения. Для них важны явные действия, предсказуемое поведение программы и возможность использовать язык близко к аппаратуре.
Но дальше их цели заметно расходятся. Zig создаётся как язык общего назначения для множества архитектур и операционных систем. Sekura JS развивается как часть собственного программно-аппаратного стека, где результат компиляции должен быть пригоден для последующей формальной проверки.
Почему Zig интересен для сравнения
В официальном описании Zig простота и явность названы одними из основных принципов языка. В нём нет скрытого выделения памяти и скрытых переходов управления, а управление памятью остаётся ответственностью программы.
Это делает Zig интересным именно в сравнении с Sekura JS.
Оба языка исходят из того, что системному разработчику полезно видеть стоимость и последствия выполняемых операций. Если программа выделяет память, обращается к функции или выполняет определённое действие, желательно, чтобы это было понятно из самого кода.
Такой подход отличается от языков, где значительная часть работы может происходить автоматически и оставаться скрытой за языковыми конструкциями.
Явность как общее свойство
Sekura JS также не стремится скрывать архитектуру машины.
В языке есть явная работа с памятью, указателями, массивами и структурами. Используются знаковые и беззнаковые целочисленные типы размером 8, 16 и 32 бита.
Программист работает с моделью, близкой к архитектуре Memora8. Расположение данных и машинное представление имеют значение и являются частью устройства языка.
Поэтому на уровне общей философии между Sekura JS и Zig действительно есть сходство: чем меньше неожиданного скрытого поведения, тем проще понимать программу.
Различие начинается с платформы
Zig является языком общего назначения. Его средства разработки ориентированы на большое количество аппаратных платформ и позволяют собирать программы для различных целевых систем.
Sekura JS создаётся иначе.
Его основной целевой архитектурой является Memora8. Язык, компилятор и модель процессора разрабатываются как связанные части одной системы.
Это сознательно уменьшает универсальность.
Зато появляется возможность заранее определить вычислительную модель, размеры значений, правила работы с памятью и связь между языковыми операциями и машинными инструкциями.
Для Sekura JS такая определённость нужна прежде всего для формальной проверки.
Работа с памятью
Zig не выполняет управление памятью за программиста. Функции и структуры данных, которым требуется динамическая память, получают средство выделения памяти явно. Такой подход позволяет использовать язык и в средах, где нет обычной операционной системы.
В Sekura JS также используется явная память, однако устройство языка ещё теснее связано с машинной моделью Memora8.
Указатель представляет адрес в 32-разрядном пространстве. При работе с массивами учитывается размер элемента, а при обращении к структурам — размещение её полей.
То есть в обоих языках разработчик имеет низкоуровневый контроль, но этот контроль используется в разных архитектурных условиях.
Zig должен оставаться пригодным для множества систем. Sekura JS может опираться на заранее определённую платформу.
Что происходит после компиляции
Здесь появляется главное различие.
Для Zig результатом работы компилятора является программа или библиотека для выбранной платформы. Далее качество программы обеспечивается обычными инженерными средствами: тестированием, проверками во время выполнения, анализом кода и другими методами.
В Sekura JS машинный результат компиляции рассматривается ещё и как объект формальной проверки.
Исходная программа преобразуется в SOBJ — машинный объект для Memora8. Отдельно задаётся формальное требование SJV.
После этого проверяется, соответствует ли фактическое поведение машинного кода заданному свойству.
Таким образом, компиляция в Sekura JS не обязательно является последним этапом перед исполнением программы.
После неё может начинаться доказательная проверка.
Почему проверяется именно машинный объект
Можно проверять свойства исходного текста программы, но между исходным кодом и процессором находится компилятор.
Если компилятор допустил ошибку при выборе инструкции, размещении данных или выполнении оптимизации, правильность исходного текста сама по себе не гарантирует правильность машинного результата.
Поэтому в Sekura JS проверяется полученный SOBJ.
SJV использует формальное требование и модель команд Memora8, чтобы исследовать поведение машинного кода.
Если существует состояние, нарушающее заданное свойство, проверка должна его обнаружить. Если нарушение невозможно в заданной области, свойство получает формальное подтверждение.
Простота языка нужна не только человеку
В Zig явность помогает разработчику понимать программу и её стоимость. Официальное описание языка прямо подчёркивает отсутствие скрытого управления потоком и скрытого выделения памяти.
В Sekura JS у простоты есть ещё одна цель.
Программу должен понимать не только человек, но и средство формальной проверки.
Чем меньше возможных трактовок имеет языковая конструкция, тем проще связать её с машинным кодом и затем с математической моделью.
Поэтому ограниченность Sekura JS рассматривается не только как способ сделать язык проще. Это часть общей задачи построения проверяемого стека.
Модули и границы системы
Sekura JS строится вокруг явной модульной модели.
Один исходный файл описывает один модуль. Для него могут формироваться машинный объект, сведения о размещении данных и описание доступного интерфейса.
Такое устройство помогает определять границы между частями системы.
Для формальной проверки это особенно важно. Можно связать требование не со всей программой сразу, а с конкретным модулем и конкретным результатом его компиляции.
Zig также позволяет строить крупные модульные программы, но его организация не определяется задачей создания доказательной цепочки для конкретной аппаратной архитектуры.
Оптимизация и сохранение поведения
Оба языка имеют компилятор, который может преобразовывать программу для получения более подходящего машинного кода.
В Sekura JS нас интересует дополнительный вопрос: сохранилось ли после этих преобразований формально заданное свойство.
Поэтому одна и та же исходная программа может быть скомпилирована с разными уровнями оптимизации, а каждый полученный машинный объект проверен относительно одного и того же требования.
Так оптимизатор не становится полностью доверенной частью цепочки.
Его результат можно проверять отдельно.
Почему не использовать просто Zig
Если задача состоит в разработке обычного системного программного обеспечения для существующих архитектур, Zig предлагает значительно более широкие возможности и готовую поддержку множества платформ. На официальном сайте он прямо позиционируется как язык общего назначения и набор средств для создания надёжного и переносимого программного обеспечения.
Sekura JS решает более узкую задачу.
Он создаётся одновременно с Memora8, системным программным обеспечением Reganta и средствами формальной проверки.
Поэтому от него не требуется быть универсальным языком для всех существующих платформ.
Требуется другое: сохранять достаточно простую и определённую связь между исходной программой, машинным кодом и формальным свойством.
Два варианта явного системного языка
Sekura JS и Zig показывают, что идея простого и явного системного языка может использоваться для разных целей.
В Zig явность помогает создавать переносимое низкоуровневое программное обеспечение без скрытого управления памятью и потоком выполнения. Язык при этом остаётся рассчитанным на широкий набор архитектур и задач.
Sekura JS использует схожий принцип явности, но внутри значительно более узкой системы.
Его задача — не только создать понятный машинный код, но и связать этот код с формальным требованием и проверить его относительно модели процессора Memora8.
Поэтому главное различие можно сформулировать просто.
Zig стремится дать явный и универсальный инструмент системного программирования. Sekura JS использует явность как основу для построения программного слоя формально проверяемого стека.
Именно эта цель определяет устройство Sekura JS и объясняет, почему язык сознательно остаётся тесно связанным с собственной аппаратной платформой.
Share
