I'd be really happy to see seL4 thrive and I like that this blog-post shows that the people behind it understand what could potential hold it back - the infrastructure around it. It needs what GNU and systemd are for Linux. And it needs an Arduino/Raspberry Pi - a halo platform that I can buy and play around with.
What I wonder is how this formal verification works. seL4 is written in C and apparently the formal verification is done in a different language. Is it possible to have a programming language where the compiler does the formal verification?
What I wonder is how this formal verification works. seL4 is written in C and apparently the formal verification is done in a different language. Is it possible to have a programming language where the compiler does the formal verification?