> On the other hand, there are correct programs which we still don't know how to type. This means that there are programs we just can't write in statically typed languages, at least not yet.
I don't think that's right. If something can't be type-checked then you just add an "assert" and do the check dynamically.
For example, in 0install I need to ask the SAT solver which version of a program I should use. I pass it a load of SAT variables, each containing a user data field with the attached program details, run the solver, and get back the selected variable. The SAT problem also contains other variables, with other kinds of data.
I know the user data field for the selected result will be of type program details, but I couldn't figure out how to let the compiler check this statically. It's not a problem; I just check the type and "assert false" if it's wrong. I still get the benefit of static checking almost everywhere else in the code.
I don't think that's right. If something can't be type-checked then you just add an "assert" and do the check dynamically.
For example, in 0install I need to ask the SAT solver which version of a program I should use. I pass it a load of SAT variables, each containing a user data field with the attached program details, run the solver, and get back the selected variable. The SAT problem also contains other variables, with other kinds of data.
I know the user data field for the selected result will be of type program details, but I couldn't figure out how to let the compiler check this statically. It's not a problem; I just check the type and "assert false" if it's wrong. I still get the benefit of static checking almost everywhere else in the code.