I'm looking for a computer langauge with "dependent types" but...
The problem with it having a full implementation is that you end up having to write formal type proofs to get even anything simple done. (Agda/Iris). These are fine if you are writing a proof checker but not for general programming.
As a compromise it would be nice to have a language that would allow "unsafe" dependent type casting where you don't have to give a proof. e.g. you might have a type "PrimesBiggerThan3" and a type "OddNumbers" and you could cast from the first to the second without having to give a formal Type Proof. The proof could just say "TrustMeOnThis".
Does such a language exist, or is there one like this that is useful?