Сделал вот (де)мотиватор

[elder_george]

Comments

[skalych]

Он наверное сейчас начальнег и пользуется... эээ... кнутом. :)

[elder_george]

Скорее, как-то так:

[blackyblack]

Он ещё и программы доказывает... Не во всём следует брать с него пример :)

[elder_george]

Ты так говоришь, как будто в этом есть что-то плохое =)

[katrin_elinor]

Потрясающе! =)
А у нас на кой-то аж три курса по формальной верификации было. Интересно, ей кто-нибудь промышленно пользуется? По-моему, это даже для простых программ, типа алгоритма Евклида, тот еще геморрой. А для параллельных программ - вообще страсть.

[elder_george]

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

Другой вопрос, что составление формальной и непротиворечивой спецификации для многих программ сопоставимо по сложности с написанием самой программы. В этом смысле, разработчики трансляторов (типа Кнута) и ОС в привилегированном положении =)