I'm not an abstract thinker so that correspondence is not interesting to me (open to being educated though if it is applicable to my daily work), but to what ridiculous beliefs do you refer? TIA
I don't really have a glossary or nosology of how people misuse this, but I'd say some wrong ideas include:
* If a language has a type system, then it is usable for formal proofs, it is sound, and it is a language that ends the need for other languages.
* Dependently-typed languages have values that are also types, so all values are types, and therefore dependent typing makes no sense.
* Because my language uses higher-order logic instead of first-order logic, Turing's results don't limit my language's problem-solving abilities.
* Because of my religious beliefs, type universes have a certain shape, and thus Cantor's results are incorrect.
* The English language is far more powerful than any programming language.
* All logic is really just intuitionistic logic.
* All logic is really just linear logic.
* Syntactic formalism must be wrong, because abstracta only exist in my mind.
To repeat myself, all of these are wrong, despite some relatively large tribes of programmers believing them sincerely.
[0] https://ncatlab.org/nlab/show/relation+between+type+theory+a...
Obviously it's all really just tensorial logic :^)
> * All logic is really just linear logic.
and
> * Because of my religious beliefs, type universes have a certain shape, and thus Cantor's results are incorrect.
> All logic is really just linear logic.
Who has said these?
��Curry-Howard is the idea that static types are propositional formulas and expressions that have such types are their proofs. Under the Curry-Howard correspondence, a static typechecker analyzing your program is equivalent to a proof checker ensuring that your proof is valid.
People tend to invoke Curry-Howard to praise ML- and Haskell-style algebraic types (according to Curry-Howard, sum types are disjunction, product types are conjunction, and function/exponential types are implication).
Not entirely. There are type errors that are caught at compilation time.
A stark difference is that Lisp has the idea that type checking is done on values, not on symbols. If the compiler can deduce that a value is going to conflict in a given context, it will flag the error.
And types are checked at run time as well.