The Crystal Programming Language Forum

Technical word for a program that compiles re typing?

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 :smiley:

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