I don't know about this. Even some of the people who use dependently typed proof assistants seem to doubt that they should be used much in the programming part

I don't know about this. Even some of the people who use dependently typed proof assistants seem to doubt that they should be used much in the programming part (as opposed to the proving part). Also, some of the examples you give might be addressed well enough by Rust's const generics. https://xenaproject.wordpress.com/2020/07/05/division-by-zero-in-type-theory-a-faq/ https://xenaproject.wordpress.com/2020/07/05/division-by-zer... https://www.cs.ox.ac.uk/ralf.hinze/WG2.8/26/slides/xavier.pdf https://www.cs.ox.ac.uk/ralf.hinze/WG2.8/26/slides/xavier.pd...