Why do you think so? It's a completely standard usage. For example, we can ask MathWorld:
> In logic, a term is a variable ['a', 'f'], constant ['1', '"hello"'], or the result of acting on variables and constants by function symbols ['1+2', 'f(a)'].
(I've added the bracketed material, which provides examples of the senses that MathWorld gives. https://mathworld.wolfram.com/Term.html )
In particular, note that by this wording, if you're looking at '1+2', the "term" is not the string '"1+2"' but the result of adding '1' to '2', which is '3'.
You can talk about 'terms' in the context of how a compiler views source code. Or you can talk about 'terms' in the context of how type theory applies to some computation. They'll be called 'terms' either way; you seem to have staked out the position that the compiler context is obligatory and the type theory context is somehow in error.
In fact the "Calculus of Constructions" (CoC) derived from Typed Lambda Calculus unifies everything into a Term like so;
Term ::= variable | lambda abstraction | lambda application | dependant product | sorts (type of types)
For reference see Brandl's work that i list here - https://news.ycombinator.com/item?id=50028902
In Computation this is just made explicit and clear using a "eval function".
Do you seriously want to argue this point?
> you seem to have staked out the position that the compiler context is obligatory and the type theory context is somehow in error.
I used the compiler to illustrate the issue to people who clearly aren’t familiar with type theory. You imply that you are, but in that case, how do you justify the nonsense quoted above?
> Types are groups of related values.
This is an operational perspective which misses one of the most important aspects of types: in a statically typed language, types are a way to classify terms, i.e. they're not just about values.
As an example of why this distinction matters, consider this expression: 1 + "hello". In most statically typed languages, this will be rejected at compile time. It doesn't have to be evaluated (i.e. at runtime) to be rejected - it's invalid because the types of the terms - 1 and "hello" - aren't compatible.
This compile-time rejection is only possibly because types apply to terms, and terms aren't values. This is critical to the usefulness of statically-typed languages - without this, they'd have to run the program to detect type errors.
Benjamin Pierce's book "Types and Programming Languages" has some great coverage of this topic.
In "Simply Typed Lambda Calculus" (STLC) there are two grammars for a legal expression.
1) Type Grammar - Type ::= inbuilt types | Type1->Type2 (function)
2) Term Grammar - Term ::= constant | variable | lambda abstraction : "Type" | lambda application.
Note how in (2) above "Type" comes into the picture. During compilation, the expression's structure is analyzed and verified against the Typing Rules aka "Type Checking". Once this is passed the expression is considered sound and can be evaluated at runtime.
In "Calculus of Constructions" (CoC) the two grammars are unified into one which gives us powerful concepts like dependent types, polymorphism etc. - https://news.ycombinator.com/item?id=50137880
Also, 1 + "hello" is "1hello", obviously. Have you never read JavaScript? :)
What trips us up is having existing expectations for what an operator called + should do.
Exactly. And if that were the case, you couldn't do very much type checking at compile time.
Javascript, or more specifically Typescript, is precisely why I wrote "In most statically typed languages..."
In Typescript, you can write `1 + "hello"` and the type system will infer that the type of that term is 'string'. It doesn't change anything I wrote above.