Comment by qazxcvbnm

Just to further clarify on the reasons why I think that work into such computational models are badly needed; I think that comprehensible systems fundamentally possess a kind of impedance mismatch with natural forms of expression within von Neumann architecture (as noted elsewhere in the comments). For many years, functional programmers and computer scientists have looked forward to the immense performance potential of automatic parallelisation of pure terms over imperative operations, due to explicit declarations of data dependencies - but despite the passing of decades, it is yet to be fulfilled. Probably no one would consider functional languages for the most performance sensitive of tasks.

As is well known in functional programming circles, mutation and non-referentially transparent operations make systems non-composable and incomprehensible. Pure, composable computation can generally be roughly modelled as terms in lambda calculus. However, elegant as lambda calculus may be as a computational model for computer scientists, to a rough approximation, CPU instructions resemble more of Turing machines. To a very rough approximation, we can take each CPU instruction to cost O(1) time, but on the other hand, lambda reduction takes a much more complex and variable cost depending on your term and reduction strategy, and is highly non-local. The potential of Interaction Nets lies in part, in allowing evaluation of lambda terms in essentially O(1) time.

Of course, Linear Logic reveals that many other facets regarding the efficiency of term evaluation are also deeply intertwined, and besides new solutions to evaluation steps and time-cost, Interaction Nets simultaneously act in a way which is local (allowing embarrassing parallelisation, and thus the whole possibility of HVM's GPU backend for arbitrary computation, albeit I believe, in progress) and also allows automatic erasure of unnecessary terms in large classes of terms (automatic garbage collection).

Together, the problems that Interaction Nets solve seem to altogether make the tradeoff between comprehensibility and efficiency an unnecessary choice.