Я и не сомневаюсь что можно, вопрос насколько это будет красиво. Если эта формализация позволит найти ошибки / доказать что их нет - да, поменяю, безусловно.
Придётся, конечно, закопаться в операционную семантику, с которой работать, скажем так, не очень приятно, но только так получится формализовать non-local return.
@noraltavir у тебя нет, случайно, свободных студентов?