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

Я периодически тоже задумываюсь о системах, где можно было бы проследить связь требований (спецификаций), реализации (кода в моем случае) и евиднесов (тестов и результатов тестирования). И как-то у меня в голове это слабо сходиться, не конвергируется. Сдается мне, что чтобы конвергировало, нужно все формализовать на Higher Order Logic. Ибо нужно работать с циклами и цепочками произвольной длинны. Т.е. система должна поддерживать рассуждения о множествах в том или ином виде. Боюсь что First Order тут не хватит. Т.е. отдельные фрагменты можно и нужно апроксимировать простыми формалистиками. Но вот когда начинаешь собирать все в кучу... Формализация всего на математическом языке Higher Order Logic - самый трудный путь из тех, что можно представить, но, как мне кажется, самый легкий из реальных. На языке онтологий это можно сказать так: хочется везде импользовать OWL DL, но при попытках обобщить, проинтегрировать и перейти на мета-уровень начинаешь понимать, что нужен OWL Full.