[Oberon] Multiple RETURN in a procedure

[Skulski, Wojciech]

Diego Sardina wrote:
> In structured programming and in formal verification of programs the return statement is a mistake and it's a fact, not a personal view.

1) Would you mind to provide a proof of your statement? It seems a bit unfounded at this point. Especially the "it is a fact" portion.

2) I have not heard whether formal verification was ever applied to a the actual Oberon System 2013. We all probably care whether it works or not, rather than whether it can be formally verified, and what it would mean if it was verified.

Wojtek