Без заголовка

Как я понимаю, все эти 5 пунктов про Coq -- это пока только сослагательное наклонение, хотя много кода уже написано. Но и система Пиумарты уже содержит много кода, и тоже вся в сослагательном наклонении. Не сослагательное. Более точно: 1. библиотеки парсеров зрелые и давно существуют. ОКамловские используются в реальных проектах точно. 2. системы типов в Хаскел/МЛ рабочие. Это вполне зрелые языки. Так что АСТ реализуется на них легко. 3. Coq как система верифкации - зрелая по факту того, что верифицировали реальный компилятор Си. И книгу пишут. 4. Императивная библиотечка пока незрелая. Но дело в том, что императивности в моделях лучше избегать как черта лысого. 5. Хаскел реально гоняется на многоядерных системах, не так давно сделали. Но это опять-таки задел на будущее. На текущий момент в йазыковых капищах это нахрен не нужно, но на перспективу задел есть хороший. Уже есть стартап несущий депендент типы в массы http://www.impredicative.com/ur/ Там разумеется есть много проблем, но это не проблема для стартап деятельности, а как раз наоборот - стартап ведь и призван решить какую-то проблему. Я к тому что фундаментальные подходы готовы и тулзы есть, пора заниматься внедрением в обычную жизнь. Я вот сейчас серьезно задумываюсь о создании инструментария для парсенья Жабы (каких-то подмножеств), чтобы можно было автоматически верифицировать/тестировать на простые баги. Такие инструментарии есть, но они промышленно не юзабельны, ибо: 1. не поддерживают Жабу 1.5 2. нет автомтических детекторов инвариантов (что означает проблемы с циклами) 3. Жабные библиотеки не специфицрованы формально Первый пункт решить несложно - по крайней мере, надо чтобы входной код разбирался, пусть без формальных выводов. Второй пункт сложнее, но я тут буду думать как Coq применять, похоже там можно найти полу-автоматическое решение. Третий пункт - вопрос времени, если предыдущие два решить, то формализации библиотек можно потихоньку наращивать.