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

В Language Workbenches нужен базовый язык (формализм я бы даже сказал), и соответственно он определяет общие свойства воркбенча. HOL тут наиболее выразительный формализм, следовательно Воркбенч на ее основе будет наиболее выразительным. Правда потенциально, ибо на реализацию выразительности будут затраты. Зато всегда можно (затратив определенные усилия) транслировать одну парадигму в другую. Собсно, транслировать-то можно хоть на Си, вопрос в кол-ве усилий (и багов). А HOL позволяет сертифицировать трансляцию, т.е. можно хоть как-то управлять такой неимоверно сложной штукой как Воркбенч: в общем случае, сложность растет квадратично от кол-ва языков). А если есть верификация, то путем трансляции через промежуточный язык получаем линейную сложность.