Yes, they are commonly used in formal languages, and their precise meaning is language dependent, which is why I didn't use partial or divergence but terminatio

Yes, they are commonly used in formal languages, and their precise meaning is language dependent, which is why I didn't use partial or divergence but termination, which has a unique computational meaning. I don't think anyone claims that any property can be proven. I do think that some think that if a program can be decomposed into simple parts, whose "interesting" properties are provable in isolation, then you can feasibly prove interesting properties of their composition, which is not true. A proof of that was only given in the past 10-15 years, and is referenced in my post.