Stupid questions:
1. instead of doing research for proving correctness wouldn't it be better to write everything in Rust like you say?
2. even if your system is full of bugs if you limit your exposure to the external world to a small set of secure gateways won't that mostly fix it?
Provable correctness was IMHO a dead end. Too hard. Which is why your question (1) seemed like the better compromise.
Secure gateways only help if the data is processed by them, not just passed through. Firewalls don't really help, as soon as you open a single port, anything can get through it. I'm on an Oracle-owned patent for a "secure data broker" which sits in a firewall and inspects the data coming through, validating it against an XML schema before passing it on to the internal-network destination computer. https://patents.google.com/patent/US7620980
