Навеяно веткой Интересная статья Парнаса о верификации программ

Автор: LaptevVV
Дата: 09.02.10

. Чтобы не оффтопить, вынес сюда.

Исходный посыл (deniok):

Уже всем давно понятно, что современные мейнстримовые языки должны умереть — у них абстракции текут; нет определенной формальной семантики, только стандарты "юридического" качества; ПО на них написанное без аннотирования, требующего работы на порядок бОльшей, чем затрачено на его написание, не допускает мало-мальски содержательного формального анализа.

Вопрос: а как вы представляете формальные ЯП, способные потеснить сегодняшний мейнстрим?

Я вот никак, по ряду причин:

1) Как уже упоминалоь где-то рядом, разработка ПО хорошо так специализирована. Что хорошо для "ПО на выброс", то не пойдёт в корпоратив и наоборот. Сегодняшний мейнстрим — жуткая солянка, где каждый язык хорош в своей нише и недостаточно силён, чтобы влезть в чужую.
1.1) На самом деле, слегка неправильно вообще говорить только об ЯП в контексте "кто кого заборет". Сопутствующий toolset и возможность взаимодёйствия с внешним API зачастую куда важнее всех фишек языка, особенно если mind model не совпадают.

2) Мейнстрим такой мейнстрим — либо решаем насущные задачи быстро/легко/дёшево/поддерживаемо (нужное зачеркнуть), либо в мейнстрим не лезем. А из насущных задач у нас что?
а) докрутить TUniversalComponent до рабочего состояния
б) автоматизировать бардак
в) как бы изловчиться и пнуть чужую систему чтобы она заработала.
г) найти ошибку в сложной логике с кучей условий и неочевидным code flow.
Как тут помогут формальные ЯП — хз.
2.1) Единственный почти декларативный мейнстримовый язык — SQL — хорошо показывает результат "хорошая идея vs суровая действительность".

3) Практически весь "свежий мейнстрим" — либо императивщина + чуть-чуть фп, либо декларативные высокоуровневые протоколы/стандарты описания данных (читай XML). На описание семантики никто не замахивается. Т.к. много их, ваших семантик. Плюс потихоньку пролазит декларативщина на низкий уровень, главным образом для описания state-машин (описание драйверов в сингулярити, Axum)

4) Если посмотреть на "мейнстрим из завтра", то у нас чётко видно 2 направления: виртуализация чего только можно и смесь DSL с императивщиной. На "формальная модель->код" никто пока не замахивается.

5) Возможность формальной валидации тьюринг-полного языка очень и очень сомнительна из-за нереальной размерности пространства состояний и слишком сложной формальной модели (по сравнению с реализацией "в лоб").
5.1) Валидность формальной модели вовсе не означает отсутствие ошибок в алгоритме, т.е. решающего превосходства формального подхода что-то не видно.