brencurrently 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?
cpli@brendan0x5 don't know about "binary proofs", but to my knowledge most of the work is spent proving correctness of protocols rather than implementation per se. i.e. slapping http://cyclone.thelanguage.org/wiki/Cyclone%20for%20C%20Programmers/#Regions onto C doesn't exactly make #seL4 an easier project imo