Программирования под доказательство - это составление программы и её составных частей таким образом, чтобы её корректность по отношению к спецификации можно было доказать.

Это единственный подход, позволяющий доказывать корректность программ, потому что невозможно  создать метод для доказательства или опроверженияпроизвольногокода. Типичным ошибочным выводом из невозможности доказать произвольный код, является утверждение о невозможности доказать вообще любой код.

Рассмотрим пример.
Есть спецификация на функцию:
## Код:
```
/*@ ensures \result == a; */
int func(int a);
```
Совершим невозможное:
## Код:
```
/*@ ensures \result == a; */
int func(int a) {
     return a;
}
```
Что это? Это код на C и ACSL. ПО для подтверждения корректности кода на Си и больше примеров невозможного можно найти здесьhttps://frama-c.com/wp.html. Кстати, попробуйте угадать, что означает wp.

Следующим шагом на пути осознания доказательства корректности программ, является утверждение о том, что оно применимо только кпростым случаям. Почему? Потому что в учебных материалах представлены только относительно простые примеры.

Тем не менее, не все об этом знают, и одни такие незнайки попытались доказать корректность микроядра операционной системы. Что из этого получилось, можно узнать наhttps://sel4.systems/.

Полное доказательство корректности программ полуавтоматическими средствами - это сложно и трудоёмко, тем не менее оно возможно и применяется впромышленности. Написание программ под доказательство без проведения полного подтверждения - это эффективный способ создания обычных программ. Но не стоит об этом спрашивать у среднестатистических профессионалов, пишущих на условном Javascript. Лучше спросите у них про пошаговый отладчик, ведь это основы.