I believe I proposed that somewhere because it was a small, useful app which often opened malicious payloads. People may or may not fully prove it. What I thou

I believe I proposed that somewhere because it was a small, useful app which often opened malicious payloads. People may or may not fully prove it. What I thought would be useful is, like Ironsides DNS, a SPARK Ada or other implementation that shows no code injections could ever happen from loading, modifying, or rendering text. That's a useful subset of full verification. If not that verified, writing things in a memory-safe, concurrecy-safe language covers lots of ground. Rust and Pony put good effort in those areas. In Rust, I think you still had to manually turn on checks for some overflows which hurt performance a lot. So, static analyzers or automated provers for range properties have a performance benefit. Muen is the largest, production project I know in such a language: https://muen.sk/ https://muen.sk/ Ironsides was an earlier project: https://ironsides.martincarlisle.com/ https://ironsides.martincarlisle.com/