Безупречное программирование

«В каждой программе есть хотя бы одна ошибка», «невозможно создавать программы без ошибок», бла-бла-бла… Это истинно лишь настолько, насколько вы сами в это верите. Хорошая новость в том, что существует формальное доказательство отрицания тезиса «невозможно создавать программы без ошибок», а также соответствующие контрпримеры. Но вера в этот популярный миф принесла и продолжает приносить айти-миру немало ущерба.

 

Начнём с того, что существуют языки программирования, для которых математически невозможно написать некорректную программу. Что означает корректность программы? Как минимум, что она завершается. Что это за языки? Coq, Agda, Idris, F*, …

 

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

 

На другом конце спектра — языки, на которых можно запрограммировать всё что угодно, но зато и степень корректности очень низкая.

 

Где-то в середине — языки наподобие Haskell или F#, создатели которых хотя бы пытаются нащупать упомянутый баланс.

 

Резюме этой заметки в том, что при выборе языка для разработки перспективного проекта (если конечно имеется потенциальная возможность такого выбора) лучше всего исходить из того, а что же конкретный язык предлагает в плане математической вычислимости. Если ничего такого в нём нету (хотя бы развитой системы статической типизации, как в C# или Java, или мощной поддержки метапрограммирования и кросс-компиляции, как в Python), то будь он хоть со стократным отрывом на пике мэйнстримовской популярности, использовать его не следует.

Поделиться статьей ...Share on Facebook0Share on Google+0Tweet about this on TwitterShare on LinkedIn0Share on VKPrint this page

Добавить комментарий

Ваш e-mail не будет опубликован. Обязательные поля помечены *