Log in

No account? Create an account
safe programming language - язык, на котором не говорят [entries|archive|friends|userinfo]

[ website | personal website ]
[ userinfo | livejournal userinfo ]
[ archive | journal archive ]
[ tags | journal tags ]

safe programming language [Jul. 3rd, 2018|09:02 am]
[Tags|, , ]

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.

[User Picture]From: thedeemon
2018-07-03 07:34 am (UTC)
There are different ways in which a language can be "safe".
Here is a couple of descriptions taken from websites of two programming languages, let's call them X and Y for now. Descriptions are informal, but it's important to note that in both cases compilers guarantee those levels of safety statically, so these are language properties, not runtime/implementation properties. I.e. we can check them and reject bad programs without actually generating any binaries to run.

"Memory Safety for a program is defined as it being impossible for the program to corrupt memory. Therefore, the safe subset of X consists only of programming language features that are guaranteed to never result in memory corruption.

Memory-safe code cannot use certain language features, such as:

Casts that break the type system.
Modification of pointer values.
Taking the address of a local variable or function parameter."

"Y is type safe
Really type safe. There’s a mathematical proof and everything.

Y is memory safe
There are no dangling pointers and no buffer overruns. The language doesn’t even have the concept of null!

There are no runtime exceptions. All exceptions have defined semantics, and they are always caught.

Data-race Free
Y doesn’t have locks nor atomic operations or anything like that. Instead, the type system ensures at compile time that your concurrent program can never have data races. So you can write highly concurrent code and never get it wrong.

This one is easy because Y has no locks at all. So they definitely don’t deadlock, because they don’t exist."
(Reply) (Thread)
[User Picture]From: beroal
2018-07-11 08:34 am (UTC)
The problem with such definitions is that they reference other terms not defined formally (memory corruption, data race). Dangling pointers are defined formally, but I am not sure that all these definitions are equivalent.

As definitions are informal, we have no way to prove their equivalence. No wonder that there are so many types of safety! If definitions differ at least in one word, they are deemed to define different notions. ☺
(Reply) (Parent) (Thread)
[User Picture]From: thedeemon
2018-07-03 07:37 am (UTC)
So I guess your definition tries to formalize "data-race free" property.
(Reply) (Thread)
[User Picture]From: beroal
2018-07-11 08:34 am (UTC)
Or memory corruption. I don't know.
(Reply) (Parent) (Thread)