The ambiguity and implementation divergences caused by implicit behavior is why I'm in favor of linear typing, with explicit function calls to destroy objects,

The ambiguity and implementation divergences caused by implicit behavior is why I'm in favor of linear typing, with explicit function calls to destroy objects, and the compiler verifies you destroy each object exactly once on each execution path (but does not introduce new behavior beyond the source code). Stack unwinding could either be removed, or call the "default destructor" of any objects when a panic occurs in a region of the code where an object is not yet destroyed.