Pretty much all languages w/ formal specifications do. The reason is that some specification claims are assumed/reasonable, proven outside the tool, or too hard

Pretty much all languages w/ formal specifications do. The reason is that some specification claims are assumed/reasonable, proven outside the tool, or too hard to handle immediately. This can also be used as a maybe later. I'm not sure what theirs are.