currently reading up on #microkernels, specifically #seL4, and have some questions. Would being written in a memory-safe language decrease the work required for implementation and binary proofs?