The post has been translated automatically. Original language: Russian
When a new system language appears, one of the first questions is obvious: why is it needed if C already exists?
In the case of Sekura JS, this is a particularly relevant question. Both languages allow you to work close to the machine, explicitly access memory, use pointers, structures, and integer types. But they were created for different tasks.
C has become a universal system language that is used on a variety of processor architectures and operating systems. Sekura JS is created as part of a specific hardware and software stack, where one of the goals is to formally verify the compilation result.
What do languages have in common?
Sekura JS does not try to completely hide the computer device from the programmer. In this sense, his approach is indeed closer to C than to languages with a large runtime environment and automatic memory management.
Sekura JS has integer types, pointers, arrays, structures, functions, and explicit memory access. The location of the data and the relationship to machine operations are important and remain visible to the developer.
This is a conscious decision. For system programming, it is important to understand not only the mathematical result of an expression, but also how data is represented in memory and how the program interacts with the processor.
The main difference starts with the goal
C is designed to write programs for a large number of different platforms. The same source code can be migrated between architectures, compilers, and operating systems if it follows the necessary rules of the language and platform.
Sekura JS is created at a different starting point. It is closely related to the Memora8 architecture and its 32-bit computing model.
This limits the versatility of the language, but at the same time reduces the number of variables between the source program and the machine on which it is to be executed.
This is important for Sekura JS, because we are interested not only in the portability of the program, but also in the ability to accurately verify the resulting machine code.
The 32-bit Sekura JS model
In Sekura JS, the computational model is built around 32-bit values. At the same time, the language supports integer types of various sizes, including 8-, 16-, and 32-bit signed and unsigned values.
The storage size and computational representation are considered separately. For example, a value can occupy one byte in memory, but participate in the calculation within the general 32-bit model.
This rule is part of the definition of the language and is related to the Memora8 machine model.
C, on the contrary, is designed for a large number of different platforms. The sizes and some properties of the base types depend on the implementation, which is a natural consequence of its portability.
Explicit memory
Both languages allow you to work with memory directly.
In C, pointers are one of the main features of system programming. They are used to work with arrays, data structures, devices, and low-level interfaces.
Sekura JS also uses an explicit pointer model. The address has a 32-bit representation, and the language allows you to specify the data type through which the memory is accessed.
For Sekura JS, this model is also important because the behavior of the program must then be presented in a form suitable for formal verification.
Predictability instead of universality
C needs to work in very different environments, from small microcontrollers to server systems. Therefore, the language leaves some of the behavior to the discretion of the specific implementation and platform.
In Sekura JS, the space is intentionally narrower. The language is created for a specific architecture and a common Sekura stack.
This allows you to make some rules more stringent and define properties in advance, which in a more universal language inevitably depend on the platform.
This choice cannot be considered an advantage of one language over another in itself. This is a consequence of different goals.
What happens after compilation
In normal C development, the source program passes through the selected compiler and turns into the machine code of the target platform. The correctness of the program is then usually checked by tests, analyzers, debugging tools, and other engineering methods.
In Sekura JS, the compilation process is specifically broken down into visible artifacts.
The source file can be converted into a text representation of machine instructions, a description of the placement of data and symbols, an executable object, and information about the interface of the module.
The main executable result is SOBJ.
It is this machine object that can then be formally checked against a given property.
Why is the compilation result checked?
This is one of the main differences between the Sekura JS approach.
The formal requirement is set separately from the program. The SJV validating tool takes the actual SOBJ created by the compiler and verifies its behavior relative to the Memora8 instruction model.
This leaves the real compiler between the source program and the proof.
If he converted the expression incorrectly, chose the wrong machine operation, or made a mistake when working with memory, checking the machine result may detect a discrepancy with the specified requirement.
In this sense, Sekura JS is designed not only as a programming language, but also as part of the proof chain.
Why can't you just use C and test it the same way?
Theoretically, formal methods can be applied to C programs, and such approaches exist.
The difference is not that C cannot be formally verified. The difference is in the original architecture of the project.
C must remain versatile and compatible with a large number of existing platforms and programs. Sekura JS can afford a narrower model because it is created simultaneously with the Memora8 processor, the Reganta system software and the SJV verification tool.
As a result, the language, the machine model, and the verification tool can evolve in concert.
Modules instead of one big program
Sekura JS is also built around an explicit modular model.
One source file describes one module. There are different module profiles, and the exported functions and data receive an explicit interface description.
This approach is needed not only for the organization of the program. It creates clear boundaries between the parts of the system, which may later have their own requirements and their own verification results.
Such boundaries are especially important for building a large testable stack.
What Sekura JS is not trying to replace
Sekura JS is not created as a universal replacement for C.
C has a huge ecosystem, with many compilers, libraries, operating systems, and hardware platforms. For the vast majority of existing system tasks, switching to a new language does not make sense on its own.
Sekura JS has a narrower goal.
It is created for an environment in which the processor, system software, and application modules should gradually be combined by a common evidence-based model.
Therefore, the question for us is not "can Sekura JS replace C".
A more precise question is different: what should be the system language if the ability to formally verify its machine result is one of the requirements for the hardware and software stack itself?
It is to answer this problem that Sekura JS is being developed.
Когда появляется новый системный язык, один из первых вопросов очевиден: зачем он нужен, если уже существует C?
В случае Sekura JS это особенно уместный вопрос. Оба языка позволяют работать близко к машине, явно обращаться к памяти, использовать указатели, структуры и целочисленные типы. Но создавались они для разных задач.
C стал универсальным системным языком, который применяется на множестве процессорных архитектур и операционных систем. Sekura JS создаётся как часть конкретного программно-аппаратного стека, где одной из целей является формальная проверка результата компиляции.
Что у языков общего
Sekura JS не пытается полностью скрыть устройство компьютера от программиста. В этом смысле его подход действительно ближе к C, чем к языкам с большой средой исполнения и автоматическим управлением памятью.
В Sekura JS есть целочисленные типы, указатели, массивы, структуры, функции и явный доступ к памяти. Расположение данных и связь с машинными операциями имеют значение и остаются видимыми для разработчика.
Это сознательное решение. Для системного программирования важно понимать не только математический результат выражения, но и то, каким образом данные представлены в памяти и как программа взаимодействует с процессором.
Главное различие начинается с цели
C предназначен для написания программ для большого количества различных платформ. Один и тот же исходный код можно переносить между архитектурами, компиляторами и операционными системами, если он соблюдает необходимые правила языка и платформы.
Sekura JS создаётся в другой исходной точке. Он тесно связан с архитектурой Memora8 и её 32-разрядной вычислительной моделью.
Это ограничивает универсальность языка, но одновременно уменьшает количество переменных между исходной программой и машиной, на которой она должна выполняться.
Для Sekura JS это важно, потому что нас интересует не только переносимость программы, но и возможность точно проверить полученный машинный код.
32-разрядная модель Sekura JS
В Sekura JS вычислительная модель строится вокруг 32-разрядных значений. При этом язык поддерживает целочисленные типы разного размера, включая 8-, 16- и 32-разрядные знаковые и беззнаковые значения.
Размер хранения и вычислительное представление при этом рассматриваются отдельно. Например, значение может занимать один байт в памяти, но участвовать в вычислении в рамках общей 32-разрядной модели.
Такое правило является частью определения языка и связано с машинной моделью Memora8.
C, напротив, рассчитан на большое количество различных платформ. Размеры и некоторые свойства базовых типов зависят от реализации, что является естественным следствием его переносимости.
Явная память
Оба языка позволяют работать с памятью напрямую.
В C указатели являются одной из основных возможностей системного программирования. Через них строится работа с массивами, структурами данных, устройствами и низкоуровневыми интерфейсами.
Sekura JS также использует явную модель указателей. Адрес имеет 32-разрядное представление, а язык позволяет задавать тип данных, через который выполняется обращение к памяти.
Для Sekura JS эта модель важна ещё и потому, что поведение программы должно затем быть представлено в форме, пригодной для формальной проверки.
Предсказуемость вместо универсальности
C должен работать в очень разных условиях: от небольших микроконтроллеров до серверных систем. Поэтому язык оставляет часть поведения на усмотрение конкретной реализации и платформы.
В Sekura JS пространство намеренно уже. Язык создаётся для определённой архитектуры и общего стека Sekura.
Это позволяет сделать некоторые правила более жёсткими и заранее определить свойства, которые в более универсальном языке неизбежно зависят от платформы.
Такой выбор нельзя считать преимуществом одного языка над другим сам по себе. Это следствие разных целей.
Что происходит после компиляции
При обычной разработке на C исходная программа проходит через выбранный компилятор и превращается в машинный код целевой платформы. Корректность программы затем обычно проверяется тестами, анализаторами, средствами отладки и другими инженерными методами.
В Sekura JS процесс компиляции специально разбит на видимые артефакты.
Исходный файл может быть преобразован в текстовое представление машинных инструкций, описание размещения данных и символов, исполняемый объект и сведения об интерфейсе модуля.
Главным исполняемым результатом является SOBJ.
Именно этот машинный объект можно затем формально проверять относительно заданного свойства.
Почему проверяется результат компиляции
Это одно из основных различий подхода Sekura JS.
Формальное требование задаётся отдельно от программы. Проверяющий инструмент SJV берёт фактический SOBJ, созданный компилятором, и проверяет его поведение относительно модели команд Memora8.
Таким образом между исходной программой и доказательством остаётся реальный компилятор.
Если он неправильно преобразовал выражение, неверно выбрал машинную операцию или допустил ошибку при работе с памятью, проверка машинного результата может обнаружить расхождение с заданным требованием.
В этом смысле Sekura JS проектируется не только как язык программирования, но и как часть доказательной цепочки.
Почему нельзя просто использовать C и проверять его так же
Теоретически формальные методы можно применять и к программам на C, и такие подходы существуют.
Разница заключается не в том, что C невозможно проверять формально. Разница в исходной архитектуре проекта.
C должен сохранять универсальность и совместимость с огромным количеством существующих платформ и программ. Sekura JS может позволить себе более узкую модель, потому что создаётся одновременно с процессором Memora8, системным программным обеспечением Reganta и средством проверки SJV.
В результате язык, машинная модель и проверяющий инструмент могут развиваться согласованно.
Модули вместо одной большой программы
Sekura JS также строится вокруг явной модульной модели.
Один исходный файл описывает один модуль. Существуют разные профили модулей, а экспортируемые функции и данные получают явное описание интерфейса.
Такой подход нужен не только для организации программы. Он создаёт понятные границы между частями системы, которые в дальнейшем могут иметь собственные требования и собственные результаты проверки.
Для построения большого проверяемого стека такие границы особенно важны.
Что Sekura JS не пытается заменить
Sekura JS не создаётся как универсальная замена C.
У C огромная экосистема, множество компиляторов, библиотек, операционных систем и аппаратных платформ. Для подавляющего большинства существующих системных задач переход на новый язык сам по себе не имеет смысла.
У Sekura JS более узкая цель.
Он создаётся для среды, в которой процессор, системное программное обеспечение и прикладные модули должны постепенно объединяться общей доказательной моделью.
Поэтому вопрос для нас звучит не как «может ли Sekura JS заменить C».
Более точный вопрос другой: каким должен быть системный язык, если возможность формально проверить его машинный результат является одним из требований к самому программно-аппаратному стеку?
Именно для ответа на эту задачу развивается Sekura JS.
Share
