Checking the validity of an argument is like typechecking: It's mostly mechanical and catches a large class of errors.

But there are some it doesn't catch. This is a valid argument:

    All animals live on Mars.
    All humans are animals.
    Therefore, all humans live on Mars.

The point being (which we both understand, but not everyone here does) is that in logical terminology, a "valid" argument is one whose conclusions must be true were its premises all true. That is a valid argument, even though its first premise is obviously false, because were its premises true, then its conclusion must be true. A valid argument whose premises are all true is a "sound" argument. But, while philosophers and logicians respect this "sound"/"valid" distinction, in popular usage the word "valid" is used to mean "sound".

All animals live on Mars? You've lost me.

IIRC, in logic, an argument is essentially a function that takes premises and produces a conclusion. It's valid as long as the conclusion follows from the premises. The catch is that an argument being valid is not the same as the conclusion being true.

That is not a valid argument, because all animals do not live on mars. Your premises have the wrong type, and you have abused them to reach a fallacious conclusion.

This is what you meant to say:

    Suppose all animals live on mars.
    Suppose all humans are animals.
    Therefore, if all animals live on mars, then all humans live on mars.

This argument passes the type-checking test, and is indeed valid.

You are confusing the distinction between validity and soundness.

> That is not a valid argument, because all animals do not live on mars

It would be more accurate to say that it is not a sound argument because all animals do not live on mars. Validity relates to whether the conclusions follow from the premises, not whether the premises are true. (There are more constraints than that, but that's the basic version.)

I am aware of the distinction between soundness and validity, but logic has strict types. I am referring to the type of the conclusion being wrong. "Therefore, all humans live on Mars" is not a valid conclusion from those premises if their truth value is not established. One must conclude the entire proposition "Therefore, if all animals live on Mars, then all humans live on Mars" for the argument to be valid.

Our strict types are Fact, Hypothetical, and Implication. It is only valid to use possibly unsound premises if you admit their type as Hypothetical and not Fact. If our argument includes premises of type Hypothetical then it is only valid to make conclusions of type Implication, which have the form "If <Hypotheticals are True> then <Fact>."

Disguising Hypothetical-type premises as Fact-type, and using that to draw conclusions of type Fact instead of type Implication is how people create strawman arguments in bad faith, and can be prevented at the validity-checking phase by enforcing strict typing.

Nah, the type is correct, it's just that the value is false, hence the conclusion will also be false, even for a valid logical argument.

I mean the type of the conclusion is wrong. If our argument includes premises of type Hypothetical then we may only make conclusions of type Implication, of the form "If <Hypotheticals are True> then <Fact>."