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

Насчёт же доказательств, думаю будет то же, что с языками формальных спецификаций типа Z. То есть применят на паре мелких проектов в полунаучной области и забудут. Отдел QA смотрит на наличие требуемых разделов в бумажке и не лезет в то, что внутрях написано.