You can write "annotate" your rust code using asserts. On the wasm side asserts are converted to trap instructions, so the Lean spec will simply be: For every input this code never traps.
Part of our focus is making sure that specs are both easy to write and read, since they are human facing. Eventually you could imagine how writing code will mostly be writing specs, and both the code and the proofs will be handled by AI agents. In this scenario it is very important that humans can easily audit and modify the specs.
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.
The reason AI has been so good at filling most of the proofs in my opinion, is that proofs are actually "simple", but very tedious and long. Part of our work right now is make sure that the tedious part can be solved mechanically as easy and efficient as possible, so both human or AI can focus on the interesting parts.
