safe programming language
Safe programming languages 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.
My definition of safe PL implementation refers to the notion of multithreading which I will not define here. Informally, a PL implementation is safe if it does not spoil the execution of other threads. A PL implementation impl is safe iff for any two threads thread_0 and thread_1 such that thread_0 runs impl, the real semantics of thread_1 is equal to its official semantics. By the official semantics of thread_1, I mean the semantics of the program that thread_1 runs according to the semantics of the PL in which that program is written. By the real semantics, I mean the behavior of thread_1 as it runs along thread_0. The real semantics may differ from the official semantics because of thread_0 interfering with thread_1, for example, writing to the memory region belonging to thread_1. As usual, semantics does not include running time or memory consumption.
My definition of safe PL implementation refers to the notion of multithreading which I will not define here. Informally, a PL implementation is safe if it does not spoil the execution of other threads. A PL implementation impl is safe iff for any two threads thread_0 and thread_1 such that thread_0 runs impl, the real semantics of thread_1 is equal to its official semantics. By the official semantics of thread_1, I mean the semantics of the program that thread_1 runs according to the semantics of the PL in which that program is written. By the real semantics, I mean the behavior of thread_1 as it runs along thread_0. The real semantics may differ from the official semantics because of thread_0 interfering with thread_1, for example, writing to the memory region belonging to thread_1. As usual, semantics does not include running time or memory consumption.