[comp.prog.thoughts] Инструмент SPARK выходит под GPL

Недавняя новость: компании Praxis и AdaCore выпускают SPARK Pro под GPL-ной лицензией. SPARK – это специальное подмножество языка Ada (существуют версии SPARK для Ada-83, Ada-95 и Ada-2005) и набор инструментов для верификации и доказательства корректности написанных на SPARK программ. Предназначен для разработки систем с чрезвычайно высокими требованиями к корректности.

Недавно миру было предъявлено публичное доказательство убойности инструмента SPARK: проект Tokeneer. Это исследовательский проект для разработки ПО биометрической идентификации: система должна была управлять входом сотрудников в защищенное помещение. Насколько я помню, в ее состав входил сервер для хранения сертификатов с биометрической аутентификацией и ПО для взаимодействия с биометрическими датчиками и для управления дверью помещения. В результате написанное ПО работало в режиме имитации – вместо разных датчиков и прочей реальной лабуды работали программные имитаторы.

В процессе разработки были выполнены следующие фазы:

• анализ требований;
• формальная спецификация (с использованием специального языка Z);
• проектирование;
• реализация на SPARK;
• верификация с использованием инструмента SPARK Examiner;
• тестирование системы.

Разработка заняла 260 дней, было написано 9939 строк кода. После поставки системы (я так понимаю, после тестирования, уже для дальнейших экспериментов) в ней было выявлено 2 ошибки. Эксперимент был признан удачным (не зря же им теперь размахивают как победным флагом).

Не берусь судить о том, насколько все это круто (все-таки всего 10K строк кода за почти год работы нескольких человек)… Ну да они там в своем монастыре, у них свои уставы.

Я о другом хочу сказать. Вот это веяние – выпуск продуктов бесплатно под GPL – это же не от хорошей жизни, имхо. Сначала EiffelStudio стали раздавать под GPL. Теперь вот SPARK (GPS – среда разработки под Ada и GNAT-компиляторы Ada уже давно под GPL ходят, насколько я знаю). Думаю, что это свидетельство того, что данные инструменты никому не нужны. Тем более за те деньги, которые за них просят. Вот и пытаются их владельцы исправить ситуацию – мол мы вам первую дозу бесплатно, только попробуйте, зацените кайф…

Дело тут, наверное, в том, что выросло целое поколение программистов (может быть не одно), которое о языках типа Ada и Eiffel даже не слышало. Даже на уровне названий. Это в начале 90-х об этих языках еще говорили. Вот, мол, Ada. На нем американские военные свои системы пишут. Или Eiffel, который с Design By Contract, и на котором системы жизнеобеспечения, и встроенные системы разрабатывают. Потом пришло время Web-а, Java, C#, массового аутсорсинга и понятия “индусский код”. Ни Ada, ни Eiffel на эту платформу не вскочили (да и не должны были по статусу). А в результате они оказались на пороге забвения (имхо).

Кому сейчас нужны эти старички? Когда вокруг такой hype вокруг волшебных свойств функционального программирования. Зачем браться за какой-то там Ada-подобный SPARK, если можно тоже самое сделать на Haskell-е и получить и корректность, и волшебное распараллеливание, и еще кучу всего хорошего и вкусного?

Так что, похоже, сейчас есть возможность понаблюдать за вымиранием динозавров (Ada и Eiffel). Не знаю, достигли ли они стадии immortality, как COBOL. Вероятно, достигли. Так что совсем они не исчезнут, но останутся для многих современных программистов такой же фольклорной страшилкой, как COBOL и Fortran.