> Soundness makes perfect sense for languages that can't be implemented on > a Turing machine. Whether or not such a thing is useful is another > matter... Languages used for specification and for modular verification are often not computable in this sense. Typing may or may not be decidable. Usefulness seems clear.