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

Тут вот мысли, как мне кажется, сходные с тем, что Вы говорите (если я правильно Вас понял): - Formal methods were applied in response to an existing development problem. - Formal methods were applied selectively. Only the most critical portions of the requirements were modele - In each case, formal methods offered a partial solution to the original problem. - In each case, the results of the study fed back into the development process to improve the product. Вообще это очень интересная тема. И в ЖЖ все чаще встречаются люди, которые серьезно занимаются Coq и Agda. Я и сам сделал проектик, близкий по теме, но больше все-таки к математике относящийся.