Ну, "годен для доказательного программирования (сиречь, дедуктивной верификации)" - это по теории получается прежде всего, "удовлетворяет структурной теореме"...
так что печать вроде как ставит кодер, воздерживающийся от иного...
А вот для верификации проверкой моделей вроде как и goto не помеха... там, правда, надо не забыть представить все существенные техтребования в виде *TL-формул...
Я скорее к тому, что вот язык, применимый для программной реализации систем в смысле Усова - он должен такие различия учитывать?.. и вообще это м.б. один из существующих языков (Хаскель или иной)?.. можно что-то с позиции CS-профессионала сказать?..