Curry-Howard-Lambek distills largely into a big table which relates type theory, category theory, formal logic, and metamathematics. This table is very precise, but high-dimensional, so that we can only take small limited slices of it. Nonetheless, the slices that we take are very formal. The important parts are well-known and published, say at [0] or [1]; extending beyond this is possible but requires care and effort. That said, once one groks the nature of the correspondence, then it becomes painfully obvious, to the point where folks who don't grok it seem block-headed.

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...

[1] http://math.ucr.edu/home/baez/rosetta.pdf