[devel] I: new package

[Vitaly Lugovsky]

 why-1.05-alt1.src.rpm ушёл в incoming.

 Это средство для автоматического доказательства аннотированных
программ (т.е. спецификация идёт внутри кода, а не отдельными
утверждениями), работает поверх Coq (и некоторых других
proof-assistant-ов). Понимает некоторое подмножество языка C (без
арифметики указателей) и подмножество Caml (без type inferrence,
и т.п.)

 A must have для любого уважающего себя программиста. Давайте
писать доказанно безошибочный код, и побольше!

 В ближайшее время в Сизиф пойдёт и система Krokatoa для
доказательства аннотированного Java-кода.