Thanks. This is exactly my point. Instead of Rust, we could use a subset of C with suitable annotations and will not require any more annotations than Rust.