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

Никаких формальных ограничений, чтобы строить сложные предикаты нет. Ведь пишут очень сложный софт и ничего. А по любой функции (а софт это тоже такая сложная функция по преобразованию входов в выходы), можно построить предикат. Тут никаких принципиальных проблем, кроме как инженерно-экономических (вопрос ресурсов) и философо-онтологических нет. Более того, ограничения обладают аддитивным свойством: т.е. если к набору ограничений добавить еще одно, то это точно так же будет набор ограничений. Поэтому в реальности, предикаты еще и проще задавать, нежели написать функцию, которая бы "вычисляла" сей предикат. Тут естественно, есть риск переограничить, так что предикат будет пустым множеством, но это решаемая проблема. Модели тоже нужно отлаживать как и программы. Вот с доказательство действительно будут проблемы, но это опять же инженерный вопрос. Грубо говоря, нефиг формулировать такие формализмы, которые трудно верифицировать :). Это вобщем-то тоже вопрос квалификации. Более того, преодоление всех этих сложностей с формулированием и верификацией и дает прекрасное и глубокое понимание требований предметной области. Даже если по этому пути продвинутся лишь частично. Например, описать входы входы и выходы, рассмотреть какие-то подмодели. Преодоление трудностей с формализацией и верификацией дает знание, которого ни у кого больше нет.