I am a #ComputerScientist who is not a trained theoretician. As such, I find #DependentTypes not only intellectually stimulating (that is, challenging) but also practically attractive (albeit potentially, at present).
Using a dependently typed language, many vexing run-time checks that pollute the code could be off-loaded to the compile-time type checking, thereby leaving the logic flow clean, concise, comprehensible, and well, you know. Off-the-cuff examples abound: matrix multiplications without run-time checks for dimensional compatibility, sorted lists that need no run-time assurances of order, etc.
But these thoughts niggle me:
• BOUNDARY—Many modern, strongly, statically typed languages, like TypeScript, Zig, etc., have type systems that are Turing complete (unintentionally and with the attendant ⊥). It would be nonsensical to transfer all computing from run-time to compile-time. So, how do we, #programmers, discern this allusive boundary?
• ERGONOMICS—At present, most dependently typed languages and simply typed languages with Turing-complete type systems have rather ill syntax for type expressions. I am tempted to save Agda from this rather sweeping swipe, but even my beloved Agda's type-level syntax could use a bit of tidying up. If language designers insist upon foisting dependent types upon us, they ought to pay attention to the syntactic ergonomics of the type-level expressions as much as they do that of the value-level expressions.
