Язык должен избегать функционала, препятствующего доказательности, и наоборот, располагать к возможности доказывать правильность кода. Соответствующие конструкции должны быть встраиваемы непосредственно в основной код, как минимум, как надстройка над основным языком, но надстройка естественная. Язык должен позволять без переписывания постепенно переходить от простого прототипа ко всё более защищённому коду.
В то же время возможность доказательства не должна быть навязчивой, так как для многих задач она избыточна, и будучи навязаной может послужить препятствием для использования языка. Обязательными должны быть только ограничения, сравнительно лёгкие для использования, подобные статической типизации.
Комментариев нет:
Отправить комментарий