Checked as well. They can only do this, because they require that heap memory owned by pointers does not get fragmented. So programmers must manage pointer offsets to each heap structure themself. Hence you never get potential pointer soup (pointers pointing to subparts and pointing to other things), which Rust resolves with pointer lifetime checking.

Also loop invariants etc must all be annotated. I would be more interested how they plan to handle IO effects or if they want to omit that.