[brandmeyer]

I totally agree, and that's what I'm getting at.

Other formal models like the lambda calculus have an advantage in that lambda functions and the type systems to work with them aren't that far removed from the machines that execute them. So the practicing software engineer doesn't have a hard time using that model directly++.

As you so demonstrated, practicing HDL engineers don't generally find the actor model to be a good mental representation of their designs. Nevertheless, even in the synthesizeable subset, the languages are formally specified using message-passing processes. They just also happen to admit non-synthesizeable designs as well.