A program that compiles is… sound regarding types?
1 Like
For me, a source code that does not compiles is not a program.
Sound is used usually to describe a rule that is correct and make sense.
I understand what you mean about the word program. It is like theorem, a theorem is a theorem, it makes no sense to talk about whether a theorem can be true or false.
However, type correctness is one of several aspects of what makes a program a program. For example, the source code has to be well-formed or syntactically correct.
To me, sound means “the compiler could not prove it false, could not reach a contradiction”. That word comes to mind to me due to type inference in the language.
What can (or can’t) be sound is the compiler/typing-rules itself. By type checking/generating a program that will fails on runtime. The program is not to blame 
I would say a valid program. But that would be ambiguos if you are referring to the spec or to just the typing aspect of it.
Let me rephrase the question then :).
A necessary condition for a listing to compile is that the types are… correct? valid? consistent? sound? Which word do you guys use?
Typechecks