This is a playground where we can confirm Intuitionistic Linear Logic over Rust. See e.g. a Wikipedia article or LLWiki for Linear Logic.
- An atomic proposition is a type parameter with the bounds
Sized + 'static. - linear implication
Limpl<A, B>= A ⊸ B
- multiplicative conjunction
One= 1Tensor<A, B>= A ⊗ B
- additive conjunction
Top= ⊤With<A, B>= A & B
- additive disjunction
Zero= 0Plus<A, B>= A ⊕ B
- exponential conjunction
Bang<A>= !A
Connectives like (-)⊥, ⅋, ⊥, and ? are out of the Intuitionistic fragment.
- No panics (e.g.
panic!,unreachable!) - No exits (e.g.
abort,exit) - No infinite loops or infinite recursions
- No unsafes (especially
mem::transmutes) - No drops other than
Bang<_>andOne - No forgets (either through
mem::forgetor throughArccycles)