jondgoodwin

You claim that a language can guarantee completely deterministic runs. How is that possible in Vale?

Important mistype. It should read: "The proof does NOT stop us from knowing that SOME programs will or will not halt.

Total functional programming indeed is another example of a valid approach to weakening cycles and thereby guaranteeing termination. Although it works for that, it is too restrictive for my taste. I am looking for less restrictive forms of weakening that allow creation of a broader range of algorithms (including "imperative") that we can still guarantee will terminate.

It is indeed grand and delightful. I am glad you enjoyed the post so much. It was every bit as much fun for me to grok and then and share with others.

AIUI actors are regularly idle. However, you are right that Pony offers a clever mechanism not offered by Erlang, which allows an actor to effectively despawn itself. I believe how it does this is to notice when no other actor has a reference to it. If no other actor has a reference to it, no one cannot send it any messages. If it has no messages in its queue and it is idle (not currently dispatched on a message), we know it will never again receive any messages, and therefore it is safe to free itself because it will never again have work to do.

Author here. You are 100% correct that Pony makes a strong claim about being deadlock-free: "It’s deadlock free. This one is easy, because Pony has no locks at all! So they definitely don’t deadlock, because they don’t exist." (from the first page of the tutorial). Sylvan Clebsch is a really smart guy and Pony is a stunning piece of engineering based on rigorous analysis. He would surely know.

So far as I can determine, this part of the claim is true: it makes no use of locks, not in the runtime and none are surfaced to the Pony programmer. The only synchronization mechanism that Pony makes use of is the MPSC queues that make possible message passing between actors. Each actor has its own queue, and it is only "active" when it has messages on its queue that need to serviced. The work-stealing scheduler will give every actor with messages an opportunity to process at least one message. When it does so, it never blocks and (hopefully) finishes with no requirement to return a result to any other actor (although it may be pass messages to other actors if it wishes).

Now consider Wikipedia's definition of a deadlock: "a deadlock is a state in which each member of a group is waiting for another member, including itself, to take action, such as sending a message or more commonly releasing a lock". Notice that deadlocks can occur not only because of locks (which Pony does not have), but also because of waiting on another actor to send a message. The wiki article lists four conditions for a deadlock, which (it turns out) can also occur in a message-passing architecture.

How would Pony trigger this sort of deadlock? Consider implementing the dining philosophers problem in Pony by having the main actor spawn five fork actors (with on-table state) and then five philosopher actors, telling each the fork actor to their left and the fork actor to their right. The philosopher actors all wake up hungry, so they reach for their left fork first, by sending it an acquire message and then effectively suspend. If the left fork A is in on-table state, it changes its state to indicate it has been acquired by a specific philosopher and sends a message back to the philosopher to say it has been acquired. That reactivates the philospher to now send an acquire message to the right fork B. But maybe by this point in time another philosopher has already acquired that right fork B as its left fork! So it sends a message back to the requesting philosopher to say it is not currently available to be acquired, try again later.

If you walk through this implications of this carefully, you will see that although every philosopher is getting activated by messages regularly, at a certain point in time it is possible that meaningful forward progress can cease for at least one philosopher. At least some philosophers will starve, because they become deadlocked in not being able to get two forks needed to eat, because they are effectively contending over access to shared resources.

The situation is semantically equivalent to when we use locks for forks instead. And if we apply Dijkstra's partial order to how the philosopher actors acquire their forks in an actor-based message passing architecture, the deadlock risk vanishes and all the philosophers have a reasonable chance, eventually, to eat and therefore guarantee eventual forward progress.

Does this explanation of an example satisfy your question?

Author here. Cool story about odd perfect examples. That said, my post is not trying to find a way to crack the halting problem, and thereby demonstrate it is not real. Turing wrote a most excellent proof, and I stand by it wholeheartedly. I even cite another famous numeric example of a program we still do not know if it will terminate for all numbers: the Collatz conjecture.

Notice my description: "Turing proved that no general algorithm can be formulated that can answer this question across all possible programs." The operative part here is "across ALL possible programs". The proof does stop us from knowing that SOME programs will or will not halt. It only stops us from being able to determine this for EVERY possible program. My post explores a very specific subset of programs that we can prove will terminate, then asks what pattern(s) underlie such programs, and then explores the use of such patterns in a variety of interesting problems. It is this last result that most intrigued me, and caused me to write about it.

Hey - I am thrilled to hear about your positive experience with interning strings. I never actually did a performance test, so I am delighted to hear your gains were substantial.

As for you questions about performance on bigger source files and twiddling optimization options, I too am curious about that. I will likely revisit those questions at some point in the future. It will be easier to do once I have baked these diagnostics into the compiler.

Absolutely agree.

Did you also read the follow-on post on transitional permissions?

Very well said. This is very much what I am after. Some common idioms in Rust or C++ just feel unnecessarily verbose to me (e.g., `<exp>.unwrap().borrow_mut()`), and I am looking for straightforward ways, often borrowed from other languages, to express the same intent more succinctly and clearly.

Thanks. I always welcome feedback and take it seriously.

> There is no available reference type that can target objects from different allocators.

Cone actually does support Rust-like, lifetime-constrained borrowed references which can do exactly that safely. Cone also supports raw pointers (however de-reference safety is the responsibility of the programmer).

I appreciate the chance to learn about your language's unique form of reference type. I am less likely to call them safe than you, no doubt because I use a different criteria for safety. A key requirement I have placed on references (vs. pointers) is that you can always de-reference them and get a valid value with no chance of exception. I don't think your references would comply with this.

A Cone programmer would need to use raw pointers to throw off the shackles of lifetime constraints but, unlike with your references, they could not expect such pointers to turn into nullptr if the object they refer to has been freed. Given the nature of Cone's design, there is no way to accomplish this mechanic with decent performance, especially given that borrowed references and raw pointers are both able to point inside an allocated object.

I do appreciate your bringing it to my attention and wish you all the best with getting others to learn about and adopt your language.