This is part of the ALFE types series.
The Label type holds an address which can be passed to the goto statement, and the possible values are defined by the actual labels that are in scope. It's somewhat like a function pointer, except that there are no arguments and no return value. It's based on the GCC labels as values extension, except there's a proper type for it instead of void*.
Labels in ALFE are local, which means that the scope of a label is the block in which it is defined. So you can't use goto to jump into a block, only out of one or within the current block. Since defining a variable creates a new block with the scope of that variable, this eliminates the problem of goto skipping variable constructors. Unless you stash a label into a Label variable and then execute the goto from outside the label's scope. That's just as evil as taking the address of a local variable and then accessing it via the pointer when the object is out of scope, though - don't do that.
I think these restrictions eliminate the most heinous abuses of goto, while still allowing the useful cases (which are themselves pretty rare).