Immediately after switching the page, it will work with CSR.
Please reload your browser to see how it works.
Example from the Versus tutorial with verification:
fn octuple(x1: i8) -> (x8: i8)
requires
-16 <= x1,
x1 < 16,
ensures
x8 == 8 * x1,
{
let x2 = x1 + x1;
let x4 = x2 + x2;
x4 + x4
}
Example using debug_assert with runtime checks: fn octuple(x1: i8) -> i8 {
debug_assert(-16 <= x1);
debug_assert(x1 < 16);
let x2 = x1 + x1;
let x4 = x2 + x2;
let x8 = x4 + x4;
debug_assert(x8 == 8 * x1);
x8
}
So maybe an example could be a bare-bones gui app with a single textbox, that does an http request to some resource (having data that is unknown at compile-time and potentially untrusted is a very common thing) and fetches an array, which is bubble-sorted and displayed in the box. The bubble sort has some intentional bug (maybe due to some off by one error, the last element remains untouched). There are unit-tests that somehow don't trigger the bug (worrying that your tests are incomplete would be a primary motivator to go for proofs). It could then show how to replace the unit tests with a proof, in the process discovering the bug and fixing it.
The example wouldn't need to go into huge detail about the proof code itself as it is potentially advanced, instead it would focus on the nitty-gritty details of adding the proof, like how the interface between proved mathematical code and non-proved io code works, what command line to run to prove&build, and finally a zip archive with all of that, that you can play around with.
Edit: Actually just reading from stdin and writing to stdout is probably good enough.
> verifying the correctness of code
What is the difference between "verifying" the correctness of code, as they say here, vs "proving" the correctness of code, as I sometimes see said elsewhere?
Also, is there a good learning resource on "proving" things about code for working programmers without a strong CS / math background?
Edit: I'm also very curious why "zero knowledge" proofs are so significant, and why this is so relevant. Eg I heard people talking about this and don't really understand why it's so cool: x.com/ZorpZK
Basically, we can prove liveness properties of the form "eventually, the controller will reconcile the cluster to the requested desired state". As you can imagine, there is a lot of subtlety and nuance to even specifying correctness here (think rapid changes to the desired state requirement, asynchrony, failures and what not).
Code: https://github.com/vmware-research/verifiable-controllers/, with a corresponding paper due to appear at OSDI 2024.