ПО без ошибок. Возможно ли это? // 15 Декабря 2012

Сможем ли мы доверять программам так же, как доверяем стенам своего дома или тормозам своего автомобиля?

Программирование считается инженерной дисциплиной, но уровень надежности конечного продукта очень отличается от результатов работы архитектора или других инженеров. Группа европейских ученых начала работу над математическим аппаратом, который позволит навсегда избавить программы от ошибок. Новая разработка на основе так называемой «теории типов», специальной области теоретической математики, должна произвести настоящую революцию в индустрии программирования.

Работа по совершенствованию программирования, как инженерной дисциплины, ведется в рамках проекта TYPES («типы»), одним из координаторов которого является профессор Бенгт Нордстрем (Bengt Nordström) из университета Чалмерса (Chalmers University) в Гетеборге, Швеция. В противовес традиционному подходу, когда качество программы проверяется в ходе длительных всесторонних тестов, ученые из проекта TYPES создают такую методику разработки, которая с самого начала гарантирует, что будущая программа будет делать то, что должна.

В проекте TYPES задействованы специалисты из 15 университетов и исследовательских институтов Европы, а еще 19 академических и промышленных организаций участвуют в программе в качестве ассоциированных участников.

Новая методика описывает задачу, которую должна выполнять программа, в виде математической теоремы. В рамках проекта TYPES также создаются открытые программные продукты, которые способны выполнять роль «проверяющих редакторов» (proof editors). Согласно теории типов, эти «проверяющие редакторы» являются гарантией правильности алгоритмов.

Может ли абстрактная математическая дисциплина обеспечить высокое качество программ на практике? Европейская математическая школа является одной из сильнейших в мире, поэтому сотрудничество теоретиков и практиков, как убеждены участники проекта TYPES, должно вывести программирование на новый уровень.

Надо заметить, все мы уже привыкли к тому, что загруженная программа не всегда делает то, что заявлено в ее описании. Если бракованную бытовую технику или автомобили со скрытыми дефектами покупатель привычно возвращает продавцу, то программные продукты окружены огромным числом «отказов от ответственности» и оговорок в лицензионных соглашениях. Новая работа европейских ученых в области теории типов и ее приложений, возможно, выведет программирование на тот же высокий уровень, который уже достигнут в других инженерных дисциплинах – в проектировании мостов и зданий, в технологиях производства различных товаров и.т.д., сообщает physorg.com.