Could you please explain what this implies in layman's terms? I've read the definition of 'linear type' as a type that must be used exactly once, and by 'mutable value semantics', I assume, that unlike Rust, multiple mutable borrows are allowed?

What's the practical implication of this - how does a Rue program differ from a Rust program? Does your method accept more valid programs than the borrow checker does?