OberonCore

У меня вдруг родилась вот какая идея. Известно, что корректную программу написать проще, если сначала формально вывести алгоритм, доказать его правильность (т.е. достижимость конечной цели и отсутствие нежелательных побочных эффектов), а затем вывести из формального определения алгоритма конкретный исходный текст программы. На этом пути есть несколько моментов, допускающих человеческую ошибку:
- доказательство правильности алгоритма может быть проведено некорректно;
- в процессе перевода алгоритма из формальной спецификации в текст на конкретном языке программирования могут быть допущены неточности или ошибки;
- особенности языка программирования могут давать побочные эффекты или вносить коррективы, не учтенные в формальной спецификации, потенциально нарушая целостность программы и её соответствие алгоритму (например, переполнение INTEGER в некоторых промежуточных вычислениях).
Почему бы нам не автоматизировать процесс перевода формальной спецификации в текст программы?

Почитав немного о языках логического программирования (например, Prolog) я обнаружил, что на таком языке можно было бы написать спецификацию, т.е. требования к пред-, постусловиям и инвариантам. Далее интерпретатор, имея некую базу знаний об алгоритмах с их пред- и постусловиями, мог бы найти решение либо констатировать отсутствие необходимой информации. В случае успешного поиска решения интерпретатор мог бы сгенерировать исходный текст на целевом императивном языке программирования (например, Oberon-2). Полученный исходный текст имел бы заранее известные, доказуемые свойства.

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

Такие товарищи как Т. Хоар пытаются создать верифицирующий компилятор. Это очень большая и сложная задача, особенно если компилировать Си или ассемблер. А что, если пойти не со стороны анализа, а со стороны синтеза? Не искать смысл в написанном коде, а писать смысл, который будет автоматически отображаться в соответствующий код.

Хотелось бы услышать мнение людей, чей кругозор не ограничивается парой-тройкой императивных языков (как у меня). Возможно ли это?

Эта идея, насколько мне известно, не нова И работы в этом направлении проводились. С несколько более глобальной идеей столкнулся в книге "Концептуальное программирование", автор Тыугу Э.Х. - 1980-х годов:

Формируется база фактов из некоторой предметной области (спец-м теоретиком), в терминах этой области (и базы) прикладной специалист (инженер) формулирует условия задачи. "Компиляция" заключается в автоматическом выводе программы-решения. Были, кажется, и языки программирования специальные разработаны.

Это и есть самая большая трудность присущая программированию. Сотворить смысл труднее всего. Именно из-за этой трудности Фредерик Брукс и заявил, что серебрянной пули нет.

Книжку поищу, спасибо! А названия языков не припомните? Желательно, в open-source-реализациях : )))

Про языки читал в самой книжке. Там даже и примеры программ были. Языки нашего, советского производства, так что насчет open-source вопрос...