I like the part that describes a high level angle of "various ways to achieve security given software development practices." It makes sense to me that PLs hav

I like the part that describes a high level angle of "various ways to achieve security given software development practices." It makes sense to me that PLs have a role to play and it would be nice if the type system were able to track capabilities. Controlling access through keys/capabilities can also be useful for memory management. This has been worked out by Crary, Walker, Morrisett "Typed Memory Management in a Calculus of Capabilities" (POPL'99). If this reminds you of Rust, it should since Rust is a practical implementation of many of these ideas (there were several papers and authors on tracking memory with types). Back to security: type systems such as the Rust one that are capable of tracking lifetimes can be used for enforcing a capability discipline. An example is GhostCell by Yanovsky, Dang, Jung, Dreyer https://plv.mpi-sws.org/rustbelt/ghostcell https://plv.mpi-sws.org/rustbelt/ghostcell subtitled "separating permissions from data" The permissions in the above references are about read/write access, but one could imagine fine-grained distinction of I/O actions being subject to a similar typing discipline. Security in type systems has been researched, with Volpano, Smith and others listed here https://en.m.wikipedia.org/wiki/Security_type_system https://en.m.wikipedia.org/wiki/Security_type_system so probably there is more. (edited for typo)