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

Кстати насчет DSL. Сейчас уже более менее зрело программирование с dependent types. Депендент тайп - типа параметризованные выражениями, например массив четных числе или массив длины 5. Фактически, депендент тайпс позволяют задавать спецификации, и явно или неявно доказывать их корректность - путем написания функции которая преобразует тип одновременно с функцией, которая преобразует входные данные. А затем компилятор проверяет валидность преобразования. Фактически неявно доказывается соответствие программы спецификации (выраженной типом). Эти языки пока новы, но их уже штук 5 минимум. Дык вот, есть такой язык/формальная система - Coq. Это система ХОЛ, поддерживающая депендент тайпс. Она весьма зрелая (на ней написали уже верифицированный компилятор подмножества Си, а один парнище пишет книгу, где убеждает что верифицированное программирование уже зрелая технология). Из программ/доказательств на этом языке, можно генерить Хаскел и МЛ код. А в Хаскел и МЛ языках есть библиотеки парсер комбинаторов - что-то типа ОМета (точнее, ОМета - это что-то вроде библиотеки парсер комбинаторов). В результате, получается что этот Coq - готовое йазыковое капище, ибо: 1 лексинг/парсинг можно вести в Хаскел/МЛ, там это легко и элегантно описывается (как в ОМета) 2 АСТ легко задается системой типов Хёдли-Милнера, которая лежит в основе Хаскел/МЛ типов 3 в Coq можно описывать преобразования из различных АСТ, задавать семантики языков, доказывать корректность и т.д. Сложности с верификацией в значительной степени облегчаются системой депендент тайпс плюс специализированными верификационным тактиками. 4 можно задавать и императивные фичи. В Хаскеле это делается монадами, которые хорошо разработаны. Монада - это такой способ инкапсуляции состояния и встраивания его в чистый функциональный язык. Для Coq есть библиотека работы с императивными монадами. 5 чистый функциональный язык типа Хаскела довольно просто кладется на многоядерность, ибо там порядок вычислений не важен, следовательно, подвыражения можно вычислять параллельно. Вобщем, компьютерная революция похоже началась и я ее немного проспал :). Хотя с Coq знаком с 2001 года.