3
$\begingroup$

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?

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.