Which is why I said to ignore RustBelt. Because we don't have formal semantics today, we only have the actual implementation which is not composable.