The post has been translated automatically. Original language: Russian
This week, a full-fledged educational circuit has appeared around Sekura JS and SJV: four textbooks, a methodological guide and a task book.
This is not a separate side job for us.
While the technology exists only in the developer's code and documentation, much of it remains understandable only to the author. The educational material forces you to build the subject anew: from simple concepts to complex ones, without omissions and hidden assumptions.
That is why the preparation of textbooks has become another test of the maturity of the language.
It was necessary to consistently explain the Sekura JS device, execution model, memory operation, functions, modules, and then move on to SJV — valid states, transitions, and formal verification of program properties.
The methodical manual sets the order of study and practical work. The task book translates theory into specific exercises: write a program, set the required behavior, check the result, find a violation and correct it.
The link between Sekura JS and SJV is also important.
Programming and formal methods are usually taught separately. At first, a person learns to write programs for a long time, and checking their properties appears much later as a special discipline.
We are trying a different approach.
The program can be viewed from two sides at once: how it works and what exactly we require of it.
It also changes the way we learn.
It is not enough to get the correct result on one example. You need to be able to formulate a program property so that it can be checked independently.
As a result, the training materials have become more than just a description of the system that has already been created. They helped to assemble language, verification, and practice into one consistent learning model.
За эту неделю вокруг Sekura JS и SJV появился полноценный учебный контур: четыре учебника, методическое пособие и задачник.
Для нас это не отдельная побочная работа.
Пока технология существует только в коде и документации разработчика, многое в ней остаётся понятным лишь автору. Учебный материал заставляет выстроить предмет заново: от простых понятий к сложным, без пропусков и скрытых допущений.
Именно поэтому подготовка учебников стала ещё одной проверкой зрелости языка.
Нужно было последовательно объяснить устройство Sekura JS, модель исполнения, работу с памятью, функции, модули и затем перейти к SJV — допустимым состояниям, переходам и формальной проверке свойств программы.
Методическое пособие задаёт порядок изучения и практической работы. Задачник переводит теорию в конкретные упражнения: написать программу, задать требуемое поведение, проверить результат, найти нарушение и исправить его.
Важна и сама связка Sekura JS с SJV.
Обычно программированию и формальным методам учат отдельно. Сначала человек долго учится писать программы, а проверка их свойств появляется значительно позже как специальная дисциплина.
Мы пробуем другой подход.
Программу можно сразу рассматривать с двух сторон: как она работает и что именно мы от неё требуем.
Это меняет и способ обучения.
Недостаточно получить правильный результат на одном примере. Нужно уметь сформулировать свойство программы так, чтобы его можно было проверить независимо.
В итоге учебные материалы стали не просто описанием уже сделанной системы. Они помогли собрать язык, верификацию и практику в одну последовательную модель обучения.
Share
