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.
TAL does use garbage collection; verifying that a GC behaves is another can of worms.