4 ms·
The correctness proof idea sounds intriguing. Ada does this already yes? And do you have any examples of where UB from unsafe rust leaks to outside the progra
by mr_00ff00 4y ago
The correctness proof idea sounds intriguing. Ada does this already yes?
And do you have any examples of where UB from unsafe rust leaks to outside the program? Surely you would look back at the unsafe code always to fix it.
- dist1ll 4y agoThere is a huge body of work around proof-based programming. If you're looking for a full blown SMT solver and general purpose dependently-typed PL have a look at F* https://fstar-lang.org https://fstar-lang.org