Maybe the real issue is the language itself.

It would be more convenient to formally identify each sub routine by a keyword, for example "sub" instead of assuming that a label is the entry of a sub.

So, instead of writing for example :

foo:
<instructions with or without labels>
return


one would write :

sub foo :
<instructions with or without labels>
return


and the compiler could easily verify that every sub has a return. The verification process should be the same as with IF THEN ELSE ENDIF for example.

But, of course, PBP is already defined...

MikeBZH