[frumplestlatz]

Curry–Howard applies when there’s a computational interpretation of proofs — like in AL, which encodes computation and abstraction in a logic.

You don’t get to do type-like work, then deny the structural analogy just because you renamed the machinery. It’s a type system built while insisting type systems are obsolete.

[practal]

You seem to know AL very well, I didn't even know that there is a computational interpretation of AL proofs! Can you tell me what it is?