I think you can do this with proof assistants, and with the SPARK version of Ada. You can also do it with a dependent type system. I haven't used it, but from

I think you can do this with proof assistants, and with the SPARK version of Ada. You can also do it with a dependent type system. I haven't used it, but from what I've read, in the ATS programming language, which is dependently typed, you can guarantee that array index accesses and pointer arithmetic never goes out of bounds, at the cost of having to pass proof variables explicitly to various functions. This poster goes over how to ensure you don't cause buffer overflows in it: https://bluishcoder.co.nz/2014/04/11/preventing-heartbleed-bugs-with-safe-languages.html https://bluishcoder.co.nz/2014/04/11/preventing-heartbleed-b... https://bluishcoder.co.nz/2018/01/10/capturing-program-invariants-in-ats.html https://bluishcoder.co.nz/2018/01/10/capturing-program-invar... It's a bit obscure; this is the only person who's ever blogged about ATS, as far as I can tell.