What’s your opinion on the scalability of formal methods? Isn’t it still the case that basically formal verification is impossible to do for larger code bases (like at least 10-100x that of sel4 in lines of code) and even sel4 took many many years and experts?

current tools, verifying C code like seL4? never going to happen. but i'm hopeful about new techniques, things like the work Amal Ahmed http://www.ccs.neu.edu/home/amal/ is doing. you don't need to formally verify the entire codebase for basic properties like "can compose with the sel4 proofs" if your runtime/compiler/language/OS is all participating. right now you have to fight against the fact that none of the software of interest is well-understood mechanically by other software.

Thanks for posting. ~yearly I look at your site (idly, not likely to have anything to contribute) because Robigalia sounded very interesting when first discussed here at https://news.ycombinator.com/item?id=10848890

ty for the kind words! i'm hoping 2021 will bring a working demo of some basic goals :) the rust ecosystem has moved a long way since 2015, async/await finally being everywhere is a gamechanger because almost everything is async/await for us!