Значит как оно в приложении к CS? Берется уже существующий язык, ну который дан, который успешен, который популярен. Ну, не знаю, пусть будет джава как конкретный пример. Мы вполне можем писать на джаве и иметь профит - но вот нам мало, по-этому мы берем какой-то формализм и описываем на нем джаву, весь ее стандарт, со всеми гофовскими паттернами и прочей хренью (но такого формализма нет, беда), причем полностью описываем, безо всяких там «подмножеств», понятное дело. Потом смотрим, и внезапно оказывается, что язык удовлетворяет какому-то свойству Х, которого мы не ожидали! И, оказывается, на нем можно делать какое-то Y, которое мы, читая стандарт языка, и не думали, что можно! Вот это и называется практическим результатом.

Если же берется какой-то готовый язык типа агды там, петуха или идриса, который изначально заточен под определенную формализацию - то тут никакого профита не будет, понятное дело, все, где написано про зависимые типы и всякие агды - это не наука, это бестолковая херня. Ну просто господа, которые занимаются CS, не могут осилить настоящие задачи, а потому переливают из пустое в порожнее - я их в этом понимаю, конечно. Статьи, диссеры, гранты - все это нахаляву, безо всякого труда, сложность работ на уровне средней школы. Кто не соблазнится? Но вот тех людей, которые это читают, нахваливают и просят еще - я понять не могу.

http://www.linux.org.ru/forum/development/9498005?cid=9592666