Ok, partially evaluate the interpreter against a python always-deadlocking program. Now it no longer implement arbitrary logic, but it is a very specific program. Yet it deadlocks.

So what does it means that Pony is deadlock free if it can implement deadlocking programs?

A better, more rigorous claim would be that the pony runtime is deadlock free or that there are no primitive blocking operations.

▲

perching_aix 4 days ago | parent [-]

Within the context of your Pony program you'll never be deadlocked. The virtual machine you implement capable of universal compute, and not enforcing this constraint, can be internally deadlocked, but this doesn't prevent your other Pony code from progressing necessarily - the deadlock is an internal state for that virtual machine, formally guaranteed to be confined to it.

I'd be hesitant to call this a "Pony runtime" property - to my understanding language runtimes just provide application bootstrapping and execution time standard library access. Pony code becomes machine code, managed by the OS as a process with some threads. This language property guarantees you that those threads will never "actually", "truly" deadlock. Code implemented on the Pony level can still progress if it chooses to do so, and Pony formally ensures it always has the option to choose so.

If your business requirements necessitate otherwise, that's a different matter, something you introduce and manage on your own.

▲

gpderetta 4 days ago | parent | next [-]

That's a bit like saying that pthreads is deadlock free because the Unix kernel can still schedule other programs. It is an useful guarantee, but it doesn't help fix my broken program.

	▲	perching_aix 4 days ago \| parent [-]
		Yes. If you want to encode soundness guarantees, you might want to look for a language with formal verification facilities instead, like Ada-SPARK. I'm not sure if there are any languages that allow you to pass down / inherit language constraints specifically, maybe Lisp or similar can do that? But then often that unfortunately wouldn't be actually helpful, as these requirements usually come from the outside (like in your Python example, it comes from Python being specified such that you can encode deadlocking logic in your Python code). For most everyone who aren't trying to implement the possibility of deadlocks in guestcode, this remains a useful property even without that.

▲

thayne 3 days ago | parent | prev [-]

You can absolutely have a pony program deadlock.

A simple example is if you get into a situation where two actors are both waiting for the other to send it a message.