Look on Starlink.com. I don't expect it's much worse than your typpical evil ISP or phone caerrier in terms of privacy. Certainly you could route everything through a VPN and that might help a little.
Edit: oh wait, I confused this thread with a different one when I looked at my inbox. Starlink is a high speed service with a roof antenna. For satellite phone stuff, look at https://skylo.tech.
Dependent types only make sense in the context of static typing, i.e. compile time. In a dependently typed language, if you have a term with type {1,2,3,4,5,6,7} and the program typechecks at compile time, you are guaranteed that there is no execution path through which that term takes on a value outside that set. You may need to supply a complicated proof to help the compiler.
In Ada you can define an integer type of range 1..7 and it is no big deal. There is no static guarantee like dependent types would give you. Instead, the runtime throws an exception if an out-of-range number gets sent there. It's simply a matter of the compiler generating extra code to do these checks.
There is a separate Ada-related tool called SPARK that can let you statically guarantee that the value stays in range. The verification method doesn't involve dependent types and you'd use the tool somewhat differently, but the end result is similar.