Locking
Locking
Posted Sep 23, 2024 20:45 UTC (Mon) by aszs (subscriber, #50252)In reply to: Locking by atnot
Parent article: Resources for learning Rust for kernel development
Not mathematician but went down a googling rabbit hole.
The terms "linear types" and "affine types" comes from substructural logic theory which in turn borrows those terms from linear and affine equations in pure math theory.
The connection is this:
linear equations are of the form 𝑓(𝑥)=𝑎𝑥 and affine are 𝑓(𝑥)=𝑎𝑥+𝑏, where 𝑎 and 𝑏 are arbitrary constants.
So in the logic:
Linear: f(x) = a*x, (x^1 as opposed to x^2...) "use x once"
Affine: f(x) = a*x + b = a*x^1 + b*x^0, "use x once or zero times".
perfectly obvious!