This was asked in the Rust Zulip as well, and is actually the original idea which this thesis evolved from (Xavier said something along the lines of "My supervisor and I have talked about how cool it would be to have a…
Ah, I knew I forgot something! Thanks, I licensed it under the MIT license now:)
It does assume enough RAM, as it has no way of knowing how much RAM the target machine will have. It is thus correct with regards to the model specified by Rust, but a program which is proven correct in Creusot may get…
Generating a proof and checking it is definitely a step up, but it does have a few issues. - SAT is in NP, and UNSAT is in CoNP. This means that proofs take a lot of space to store and a lot of time to check. Proofs are…
This was asked in the Rust Zulip as well, and is actually the original idea which this thesis evolved from (Xavier said something along the lines of "My supervisor and I have talked about how cool it would be to have a…
Ah, I knew I forgot something! Thanks, I licensed it under the MIT license now:)
It does assume enough RAM, as it has no way of knowing how much RAM the target machine will have. It is thus correct with regards to the model specified by Rust, but a program which is proven correct in Creusot may get…
Generating a proof and checking it is definitely a step up, but it does have a few issues. - SAT is in NP, and UNSAT is in CoNP. This means that proofs take a lot of space to store and a lot of time to check. Proofs are…