> These typing rules guarantee the memory safety

Huh, interesting. I'm very curious about how those typing rules ensure memory safety, presumably with neither something like Rust's borrow checker nor garbage collection. I didn't think that was possible.