https://en.wikipedia.org/wiki/Church%E2%80%93Turing_thesis

It's lambda complete. Which has been famously proven to be the same as turing complete.

Also type checking is basically more or less putting restrictions on your code. If there is a language that doesn't have the syntax to compute certain things, how would restricting that language via type checking suddenly cause it to be able to compute everything and be turing complete? Makes no sense. To make a language change from not turing complete to turing complete you have to expand.. not restrict ... but expand it's computational ability. Again Type checking serves to restrict.

Type checking is essentially just pre runtime special syntax for:

  define add (x,y)
      if type(x) != 'int' or type(y) != 'int':
           throw TypeError
      return x+2

or in a lisp like functional language:

   (define (int) (x) 
      (if (equal? type(x) 'int') (x) (error 'Type Error'))

   (define add (x y))
      (+ int(x) int(y)))

It's not a big deal. I'm not sure what LINQ is, but you don't have to add a type checking system to a language to do type checking if you know what I mean.

He doesn't know what he's talking about.