I kinda feel like this is something DARPA and the NSF should really be working on. Like, why can't we have an OS and programming environment where it's straight

I kinda feel like this is something DARPA and the NSF should really be working on. Like, why can't we have an OS and programming environment where it's straightforward to prove basic end-to-end security properties before runtime, like "this data has a `sensitive` type, and thus cannot be written to any potentially-persistent I/O facility?". I'd love it if that was something that my command shell could statically verify for me before running a job, for example.