Of course it cannot guarantee forward progress in all cases, because that would be NP.

Pony guarantees deadlock freedom by eliminating locks and other mechanisms that can lead to deadlocks. Instead, Pony uses a message-passing concurrency model and static analysis to prevent data races and deadlocks at compile time. This means developers don't need to worry about manually preventing deadlocks because the compiler handles it. The scheduler is lock-free, the order of message-delivery to all actors is guaranteed.

Here's a more detailed explanation:

Message-Passing:

Pony employs a message-passing model where actors (objects) communicate by sending messages to each other. This avoids the need for shared mutable state and locks, which are primary sources of deadlocks.

Static Analysis:

The Pony compiler performs static analysis to ensure that concurrent access to data is safe. It prevents data races and other concurrency issues that could lead to deadlocks by verifying that no two actors can simultaneously write to the same memory location.

No Locks:

Because Pony doesn't use locks, there's no possibility of threads getting stuck waiting for each other to release locks, which is a common cause of deadlocks.

Data Race Freedom:

By eliminating the possibility of data races (concurrent modification of shared mutable state), Pony also eliminates a major source of potential deadlocks.

> Because Pony doesn't use locks, there's no possibility of threads getting stuck waiting for each other to release locks, which is a common cause of deadlocks.

It may be a common cause of deadlocks, but it isn't the only way to have deadlocks.

A book I read on erlang had an entire chapter on how to avoid deadlocks with actors that had several examples of how you can get a deadlock with just message passing.

In fact, it is possible to implement a lock/mutex (also a semaphore) with actors and message passing.

sorry, that's nonsense, you can trivially deadlock without mutexes with message passing.

edit: and to be clear, I'm quite interested in Pony, static typing, shared nothing threading with message passing, capabilities, per thread GC is very close to my ideal programming language. But the bogus deadlock-freedom claim make me question the other claims.