[spoiler]Концепция типов, реализованная практически во всех компилируемых языках, заслуженно популярна, так как чем более она выразительна, тем удобнее разработчикам понимать собственный код. Нередко и проектирование системы ведется уже в терминах типов конкретной системы разработки. Этот проверенный девелоперский подход, развивающийся уже более полувека, хорошо стыкуется с методологией correct-by-construction, идея которой весьма проста: любую сколь угодно сложную корректно функционирующую систему можно получить, корректно конструируя ее из корректных подсистем. Самый тонкий тут момент -- это сам процесс конструирования (сборки), когда верифицированные модули, созданные разными разработчиками, надо состыковать через некие интерфейсы, которые должны быть гарантированно корректными. Здесь мы и добираемся до типов, которые профессор упоминает в рамках данной методологии.
API взаимодействия должен быть, условно говоря, "дубовым" -- то есть ни одна из функций не должна возвращать код ошибки вместо ожидаемого значения. Например, когда у модуля работы с базой запрашивают массив значений, а приходит отказ из-за недоступности СУБД, это неверно. Такая функция всегда должна возвращать корректный набор (значение единого типа DataSet), а он уже может быть пустым, хранить внутри себя флажки ошибок итд. Но подобная функция тем не менее будет всегда корректно отрабатывать и не вызывать сбоев в вызывающей программе. Таким же образом изолируются небезопасные указатели, неаккуратно захваченные ресурсы итп.
Условно говоря, процессов обработки ошибок в корректных программах быть не должно вообще -- просто выполняется функциональная обработка значений заданных типов (вычисления над ними), а функции обработки можно использовать только корректно и никак иначе
При этом с разработчика снимается и дополнительная забота о контроле ошибок, и обеспечение безопасности.Один из прорывов в программной инженерии пришелся на середину 1980-х, когда были появились прикладные реализации математических методов доказательства правильности программ, привязанных к механизмам проверки статической типизации. К тому же времени приходятся и первые коммерческие попытки создания программ, генерирующих программы. Удивительно, но пока не существует мэйнстримовских-коммерческих языков программирования, полноценно поддерживающих этот достаточно очевидный принцип -- correct-by-construction. На неделе стало известно о появлении correct-by-construction фишки Safe Navigation в C# http://www.pcweek.ru/idea/blog/idea/6430.php -- и то пока неизвестно, когда она воплотится в реальность. Повышение выразительности, функции как объекты, типизированные интерфейсы -- эти тренды весьма заметны в массовых языках наподобие C# и Java, но реализации их длятся годами!
Сегодня в мире ведутся активные исследования по разработке систем типов и компьютерных "помощников" программирования (proof assistants), которые охватывали бы любую вычислительную задачу и автоматически выполняли системный анализ кода независимо от общей сложности. Кстати, эта тематика тесно связана с задачами понимания естественного языка. И здесь мы плавно подходим к другой теме -- системам проверки доказательств и интеллектуальных решателей, корни которой уходят в AI, а в более отдалённой перспективе -- к программам, которые генерируют программы, и в конечном итоге, к Artificial General Intelligence.
Профессор, занимающийся этой сферой 40 лет, отмечает, что в его обязанности всегда входили прогнозы развития профильной сферы. Кратко- и долгосрочные оценки эксперта -- в следующем посте.
сами поняли что написали?