This reminds me of a suggestion I once heard that new logics like Geometry of Interaction might lead to programming languages that let you relatively cheaply understand if certain invalid states could be reached at compile time, but I haven’t had a chance to understand the real limits yet
The fact that applying Girard’s earlier work on linear logic basically led to Rust’s compile time guarantees makes me curious what else will be possible to cheaply exclude at compile time with other light twists in semantics. I wonder what it would mean to translate the above result into a PL
Comments