Computing Utility Needs Monadic Abstractions

Barbara Liskov proposed a vision of abstraction-powered Internet Computer in 2009, updating John McCarthy’s 1961 vision of utility computing. But what kinds of abstractions are needed? What fundamental problem do such abstractions aim to solve? This position paper points out a ``Liskov-Lamport chasm'' problem and argues that one type of abstractions is needed to realize a planet-scale, abstraction-powered computing utility, termed monadic abstraction. We outline three desirable properties and research goals of such abstractions: 1) a single programming concept encapsulating data, program, and machine, 2) abstraction mechanisms facilitating enforced dynamic soundness, and 3) amortized zero-cost abstractions.