This is so important. We’re always telling that we are into making things more secure, but that Rust doesn’t make software (or memory) magically bullet-proof. unsafe makes things auditable, but it is still hard.
Love how the post also gives a good guideline for auditing.
One of the brilliant things about the work formalizing the rust type theory in Coq is that they integrated unsafe into their development. It enables you to formally prove that your code sufficiently encapsulates away the uses of unsafe. If you need to use unsafe for some reason in a rust library then looking into the formal methods could be something to consider.
This is so important. We’re always telling that we are into making things more secure, but that Rust doesn’t make software (or memory) magically bullet-proof.
unsafemakes things auditable, but it is still hard.Love how the post also gives a good guideline for auditing.
One of the brilliant things about the work formalizing the rust type theory in Coq is that they integrated unsafe into their development. It enables you to formally prove that your code sufficiently encapsulates away the uses of unsafe. If you need to use unsafe for some reason in a rust library then looking into the formal methods could be something to consider.