Doesn't that put the Rust compiler (and its assert lowering) in the trusted base? How do you know the asserts you wrote are the traps you're reasoning about?
Yes, but I would argue the are already in the trusted base before this project, we are not removing that. We want instead remove "your code" from the trusted base, and just keep the compiler and the specs.
> How do you know the asserts you wrote are the traps you're reasoning about?
You just do. The asserts and the specs have a similar role, they are both consumer facing, and consumers need to make sure they are correct and cover what it is intended.