3 ms·
>and the compiler will prove to you that your functions are upholding the invariants From the article and only vague background Rust knowledge, I'm under the i
by Groxx 2y ago
>and the compiler will prove to you that your functions are upholding the invariants
From the article and only vague background Rust knowledge, I'm under the impression that the opposite is true: the compiler does not prove that. Hence why it's "assert_unchecked" - you are informing the compiler that you know more than it does.
You do get panics during debug, which is great for checking your assumptions, but that relies on you having adequate tests.
- tga_d 2y agoThat's my understanding as well. The thing I was wondering as I read it: how difficult would it be for someone to make an extension or fork of Rust that allows annotating sufficient type information to prove these kinds of invariants, like F*?