The post has been translated automatically. Original language: Russian
Artificial intelligence is noticeably changing programming.
Today, he can already write functions, fix bugs, propose architecture, create tests, and assemble entire fragments of the system. The amount of code that can be obtained in the same time is growing rapidly.
But along with this, another problem is also growing.
The code appears faster than the person has time to check it carefully.
You can ask the AI to write a program, then ask it to find errors in it and ask it again to correct the result. This is a useful working technique, but such verification remains dependent on the same class of methods used to create the program.
Therefore, it became especially important for us to separate the creation of a program and the verification of its properties.
It doesn't matter if the code was written by a human or an AI. SJV receives a ready-made program and checks it against separately specified requirements.
For example, a function should change only a certain part of the state, save the rest of the values, and return the result within the specified limits.
This requirement exists independently of the author of the code.
If the program matches it, the check confirms this. If not, the system must find a specific case of violation.
This makes the role of AI in development clearer.
He can be given more and more work on creating the program, finding solutions, and correcting the code. But trust in the result should not arise just because the answer looks convincing.
The more programs are created automatically, the more important a separate verification layer becomes.
For us, this is one of the main conclusions of recent experiments with Sekura JS and SJV.:
AI can speed up the creation of programs. Formal verification should independently answer the question of whether the resulting program meets the specified requirements.
Искусственный интеллект заметно меняет программирование.
Сегодня он уже может писать функции, исправлять ошибки, предлагать архитектуру, создавать тесты и собирать целые фрагменты системы. Объём кода, который можно получить за то же время, быстро растёт.
Но вместе с этим растёт и другая проблема.
Код появляется быстрее, чем человек успевает его внимательно проверить.
Можно попросить ИИ написать программу, затем попросить его же найти в ней ошибки и ещё раз попросить исправить результат. Это полезный рабочий приём, но такая проверка остаётся зависимой от того же класса методов, которым программа была создана.
Поэтому для нас особенно важным стало разделение создания программы и проверки её свойств.
Не имеет значения, написал код человек или ИИ. SJV получает уже готовую программу и проверяет её относительно отдельно заданных требований.
Например, функция должна изменить только определённую часть состояния, сохранить остальные значения и вернуть результат в заданных пределах.
Это требование существует независимо от автора кода.
Если программа ему соответствует, проверка это подтверждает. Если нет — система должна найти конкретный случай нарушения.
Так роль ИИ в разработке становится понятнее.
Ему можно передавать всё больше работы по созданию программы, поиску решений и исправлению кода. Но доверие к результату не должно возникать только потому, что ответ выглядит убедительно.
Чем больше программ создаётся автоматически, тем важнее становится отдельный слой проверки.
Для нас это один из главных выводов последних экспериментов с Sekura JS и SJV:
ИИ может ускорять создание программ. Формальная верификация должна независимо отвечать на вопрос, соответствует ли получившаяся программа заданным требованиям.
Share
