Не понял ссылки на реализацию в Аде. Даже самые экзотические конструкции где-нибудь, да реализованы. Но что это доказывает?
Тут дело в другом.
Я думаю, многим знакомы ситуации, когда логического выражения в заголовке цикла while не достаточно, требуется сделать еще что-то, хотя бы запомнить значения переменной. Тут начинаются муки выбора – оформить ли это вложенной функцией с побочным эффектом или испортить цикл конструкцией break/exit. Оба варианта кажутся плохими, приходится выбирать меньшее зло.
Так вот, эти мучения оказываются напрасными! Можно смело писать## Код:
```
цикл
  …
  … break
  …
конец цикла
```
При этом мы не теряем ни в строгости, ни в формализме. Аксиоматизация цикла приведена выше.