It comes from Linear Logic, where there's no inference A&B->A. I think the point of the name is "there's always progress". This talk explains some other origin

It comes from Linear Logic, where there's no inference A&B->A. I think the point of the name is "there's always progress". This talk explains some other origins as well as the connections between different logics to different type systems (though the focus is on stack languages) https://youtu.be/_IgqJr8jG8M https://youtu.be/_IgqJr8jG8M