<p>We're all used to invoking Curry–Howard to find correspondences between type systems and logical systems.</p>
<p>Rust has a very interesting type system, that is typically compared to a substructural logic. However, the concept of a &quot;lifetime&quot; doesn't seem to correspond to anything syntax-level in e.g. affine or linear logic, at least as much as I can understand them (not much).</p>
<p>The internet search yielded a <a href="https://internals.rust-lang.org/t/rust-lifetimes-semantics-at-mathematical-level/6499/11" rel="nofollow noreferrer">discussion</a> of mathematical ideas applicable to the lifetimes. However, it just talks about the mathematical properties of lifetimes. Curry-Howard bridge doesn't seem to be crossed. Are there any &quot;properly&quot; <em>logical</em> ideas that might (more-or-less) correspond to Rust lifetimes?</p>

CC BY-SA 4.0
2022-10-18T12:57:48.837Z
Probably no direct CH-correspondence. Rust's types trace back to linear types in process calculus and linear logic. Wadler's [Propositions as Sessions](https://homepages.inf.ed.ac.uk/wadler/papers/propositions-as-sessions/propositions-as-sessions.pdf) might be a place to start looking.
Martin Berger
CC BY-SA 4.0
2022-10-24T08:46:24.403Z
Maybe Taha/Nielsen's concept of [*environment classifiers*](https://dl.acm.org/doi/10.1145/640128.604134), which arose in the concept of typed meta-programming, is close enough to Rust lifetimes that Tsukadai / Igarashi's work   [A Logical Foundation for Environment Classifiers](https://arxiv.org/abs/1010.3806), which gives a CH-correspondence for ECs, could be a starting point?
Martin Berger
<linear-logic>
Is there any logical concept that Rust lifetimes correspond to?
valya
# Is there any logical concept that Rust lifetimes correspond to?

(Asked by: username_0 on 2022-10-18)

We're all used to invoking Curry–Howard to find correspondences between type systems and logical systems.

Rust has a very interesting type system, that is typically compared to a substructural logic. However, the concept of a "lifetime" doesn't seem to correspond to anything syntax-level in e.g. affine or linear logic, at least as much as I can understand them (not much).

The internet search yielded a [discussion](https://internals.rust-lang.org/t/rust-lifetimes-semantics-at-mathematical-level/6499/11) of mathematical ideas applicable to the lifetimes. However, it just talks about the mathematical properties of lifetimes. Curry-Howard bridge doesn't seem to be crossed. Are there any "properly" *logical* ideas that might (more-or-less) correspond to Rust lifetimes?

**Tags:** linear-logic
> **Comments:**
> **username_1**: Probably no direct CH-correspondence. Rust's types trace back to linear types in process calculus and linear logic. Wadler's [Propositions as Sessions](https://homepages.inf.ed.ac.uk/wadler/papers/propositions-as-sessions/propositions-as-sessions.pdf) might be a place to start looking.  
> **username_1**: Maybe Taha/Nielsen's concept of [*environment classifiers*](https://dl.acm.org/doi/10.1145/640128.604134), which arose in the concept of typed meta-programming, is close enough to Rust lifetimes that Tsukadai / Igarashi's work   [A Logical Foundation for Environment Classifiers](https://arxiv.org/abs/1010.3806), which gives a CH-correspondence for ECs, could be a starting point?  

---

## 0 answers

