Safe programming languages (PL) are gaining popularity. I wonder what is the formal definition of safe PL. For example, C is not safe, but Java is safe. I suspect that the property “safe” should be applied to a PL implementation rather than to the PL itself. If so, let’s discuss a definition of safe PL implementation. My own attempts to formalize this notion led to a strange outcome, so I would like to hear other opinions. Please, do not say that every PL has unsafe commands. We can always take a safe subset.
There is no formal definition of "safe programming language"; it's an informal notion.  Rather, languages that claim to provide safety usually provide a precise formal statement of what kind of safety is being claimed/guaranteed/provided.  For instance, the language might provide type safety, memory safety, or some other similar guarantee.