As someone who has graduate level math education and about 25 years working as a professional programmer, I emphatically disagree. A type system is itself a pr

As someone who has graduate level math education and about 25 years working as a professional programmer, I emphatically disagree. A type system is itself a programming language. If it is going to implement complex enough logic, it will be Turing complete. It does not magically become clearer simply because it ideas have been expressed in a type system. For an amusing demonstration, read through https://aphyr.com/posts/342-typing-the-technical-interview https://aphyr.com/posts/342-typing-the-technical-interview. That is a working program that solves the 8 queens problem entirely in Haskell's type system. And the type systems that you are used to are simpler in part because they are NOT Turing complete. This limits what you can say in them. In this case, for example, the author was unable to express higher derivatives as types. Now perhaps your desire is for unambiguous machine-checkable logic? If so then I highly recommend learning something like https://coq.inria.fr/ https://coq.inria.fr/. It is a worthwhile enterprise, and there are serious mathematicians who say that it, or something like it, should be implemented for all of math. However one of the objections to it is that it is harder to express and understand yourself in such systems. So unambiguous machine-checkability is a win, but not necessarily the one you thought it was. And then we come to the real issue. Are you optimizing for use, or for the person who doesn't understand the subject? It is literally impossible to think about complex things without a concise notation. The actual notation that we have has a lot of history and rough spots. But verbosity impedes comprehension. So what makes life easy for the novice and expert are exactly opposite. Also most of the use of the material is by experts, who are also who the notation is designed to be most helpful for. However even for students it helps. So much so that learning the notation generally pays off within a course or two. That is, learning the same ideas WITHOUT the notation would have been harder than learning both notation and ideas. So notation merely creates an obvious barrier, but then helps with the real one. I know you don't believe me. You've told others that it is about what works best for you. But with all due respect, you can't have any idea what actually works best for you until you've actually mastered a sufficient amount of the subject. Which you apparently haven't. Until then you are best off believing people who HAVE mastered the subject, and have spent sufficient time teaching and tutoring to know where the real barriers to understanding are for students. And everyone I know in that boat, including me, says that the notation helps more than it hurts.