> I disagree. In Coq (without axioms), it is not the case that (λx.2*x) == (λx.x+x), and programs type check fine anyway.
Type checking may be decidable in Coq but now the user has to do the work of putting things into a form that type checks. You're just pushing the problem elsewhere. Even for trivial Coq programs you have to write a large number of proofs compared to how much code you wrote.
> Speaking more generally, one of the desiderata when designing a dependent type system is to set things up so that type checking is a simpler problem than unrestricted theorem proving.
Do you know of any examples of this? I know DML limits you to linear arithmetic so type checking is decidable but that's a big limitation. All other languages like Coq, Idris and Agda require you to write proofs.
Type checking may be decidable in Coq but now the user has to do the work of putting things into a form that type checks. You're just pushing the problem elsewhere. Even for trivial Coq programs you have to write a large number of proofs compared to how much code you wrote.
> Speaking more generally, one of the desiderata when designing a dependent type system is to set things up so that type checking is a simpler problem than unrestricted theorem proving.
Do you know of any examples of this? I know DML limits you to linear arithmetic so type checking is decidable but that's a big limitation. All other languages like Coq, Idris and Agda require you to write proofs.