Без заголовка
По поводу соотношения DSL и символьных вычислений.
Различные методы символьных вычислений можно рассматривать как своеобразный DSL над системой перебора вариантов. Т.е. внутри любой технологии символьных вычислений лежит массовый перебор вариант, только оптимизированный под какой-то математический домен, будь то булева логика, или логика с ограниченным кол-вом переменных и конечными доменами (constraint satisfaction problem) или первопорядковая логика с какими-то теориями в ее рамках. А для удобства пользования этим движком есть интерфейс, который можно считать DSLем.
Далее, в современных тулзах по поддержки DSL символьные технологии играют огромную роль. Т.е. весь интеллект этих тулзов начиная от IDE кончая компиляторами базируется на символьных вычислениях, порой весьма мощных и ресурсоемких. К примеру релизы Eclipse уже год включают в себя Sat4J джавовскую SAT библиотеку, которая нужна для управления конфигурациями плагинов.
Ну и третий момент, автоматическое тестирование тоже по сути основано на символьных технологиях и тоже в какой-то мере использует DSL как сугубо тестовые (инварианты, пре-, пост-условия), так и относящиеся к решаемой проблемы (типа Mock объекты).