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

Ну с теорией-то все понятно. Абыдно, что за 15 лет ничего практичного даже в софтовой сфере не возникло, хотя оговорюсь, что все-таки может я плохо искал. Такое впечатление, что все усилия сконцентрировали на какой-то фигне вроде UMLя. Хотя опять-таки может я что-то не втыкаю. Но с другой стороны, есть ведь и обнадеживающие примеры. Подумал о примерах, и понял, что все примеры так или иначе касались моей любимой верификации :). Но это не спроста. Дело ведь в том, что все могучие идеи они как обоюдоострый меч - можно ведь порезаться и нагенерить хрен знает что. А в крупных проектах много усилий уходит именно на тестирование (до 80%). Т.е. если нагенерить кучу артефактов, то их замучаешься тестировать. Это кстати видимо основное ограничение для использования продвинутых подходов в софте типа АспектДж и т.д. И кстати, именно поэтому всякого рода тестирование выгодно автоматизировать. Ведь моделирование с целью найти коллизию на компьютере и есть такое тестирование. Т.е. на первых этапах оно все и идет в соответствии с моим опытом (софтовым). Но чтобы сделать следующий шаг, и порождать дизайн, нужно быть уверенным, что дизайн будет удовлетворять требованиям (которых дофига). А тут очень важно применять верификации. Например, верифицировать что процедура генерации соблюдает какие-то свойства. Чтобы порожденный дизайн можно было верифицировать на соответствие различным требованиям. Вобщем, меня посетила идея, что для промышленного внедрения нужно порождать proof-carrying артефакты. Которые бы можно было автоматически верифицировать на предмет критичных и важных для заказчика свойств. Тут кстати надо отметить, что производство микросхем широко основано и на порождениях и на верификациях. Т.е. дизайнеры-то работают на высоких уровнях, а потом это транслируют на более низкие (в несколько этапов). Ну и на фабриках есть спец софт для проверки их требований. Ну и т.д. и т.п.