|
|
|
|
|
|
by Dylan16807
604 days ago
|
|
|
It's more like "audit unsafe and make sure it's impossible for safe code elsewhere to lead to a violation of its assumptions". If you need to look at the safe code that calls into you when making your safety proof, then your unsafe code is incorrect and should immediately fail the audit. Treat external safe code as unknown and malicious. Prove your unsafe code is correct anyway. |
|
|