Traditional digital computing demands perfectly reliable memory and processing, so programs can build structures once then use them forever—but such deterministic execution is becoming ever more costly in large-scale systems.
By contrast, living systems, viewed as computations, naturally tolerate fallible hardware by repairing and rebuilding structures even while in use—and suggest ways to compute using massive amounts of unreliable, merely best-effort hardware.
However, we currently know little about programming without deterministic execution, in architectures where traditional models of computation—and deterministic ALife models such as the Game of Life—need not apply.
This expanded article presents ulam, a language designed to balance concurrency and programmability upon best-effort hardware, using lifelike strategies to achieve robust and scalable computations.
The article reviews challenges for traditional architecture, introduces the active-media computational model for which ulam is designed, and then presents the language itself, touching on its nomenclature and surface appearance as well as some broader aspects of robust software engineering. Several ulam examples are presented; then the article concludes with a brief consideration of the couplings between a computational model and its physical implementation.
We explore the design and implementation of Frank, a strict functional programming language with a bidirectional effect type system designed from the ground up around a novel variant of Plotkin and Pretnar’s effect handler abstraction.
Effect handlers provide an abstraction for modular effectful programming: a handler acts as an interpreter for a collection of commands whose interfaces are statically tracked by the type system. However, Frank eliminates the need for an additional effect handling construct by generalising the basic mechanism of functional abstraction itself. A function is simply the special case of a Frank operator that interprets no commands. Moreover, Frank’s operators can be multihandlers which simultaneously interpret commands from several sources at once, without disturbing the direct style of functional programming with values.
Effect typing in Frank employs a novel form of effect polymorphism which avoid mentioning effect variables in source code. This is achieved by propagating an ambient ability inwards, rather than accumulating unions of potential effects outwards.
We introduce Frank by example, and then give a formal account of the Frank type system and its semantics. We introduce Core Frank by elaborating Frank operators into functions, case expressions, and unary handlers, and then give a sound small-step operational semantics for Core Frank.
Programming with effects and handlers is in its infancy. We contribute an exploration of future possibilities, particularly in combination with other forms of rich type system.
We present instance arguments: an alternative to type classes and related features in the dependently typed, purely functional programming language/proof assistant Agda. They are a new, general type of function arguments, resolved from call-site scope in a type-directed way. The mechanism is inspired by both Scala’s implicits and Agda’s existing implicit arguments, but differs from both in important ways. [..] Unlike Scala, functions taking our new arguments are first-class citizens and can be abstracted over and manipulated in standard ways. Compared to other proposals, we avoid the pitfall of introducing a separate type-level computational model through the instance search mechanism. All values in scope are automatically candidates for instance resolution. A final novelty of our approach is that existing Agda libraries using records gain the benefits of type classes without any modification.
We present Tezos, a generic and self-amending crypto-ledger. Tezos can instantiate any blockchain based ledger. The operations of a regular blockchain are implemented as a purely functional module abstracted into a shell responsible for network operations. Bitcoin, Ethereum, Cryptonote, etc. can all be represented within Tezos by implementing the proper interface to the network layer. Most importantly, Tezos supports meta upgrades: the protocols can evolve by amending their own code. […] In addition, Tezos’s seed protocol is based on a pure proof-of-stake system and supports Turing complete smart contracts. Tezos is implemented in OCaml, a powerful functional programming language offering speed, an unambiguous syntax and semantic, and an ecosystem making Tezos a good candidate for formal proofs of correctness.
This is actually my current favorite “future technology” regarding blockchain purposes, for very specific reasons:
- I believe the DAO makes it very clear that any smart contracts network must have formal verification built in at a fundamental level.
- Listening to the StrangeLoop talk on Tezos kept me on my toes mentally the entire time, thinking of reasons it solved fundamental issues I’d had with how people had been going about what will be an intensely disruptive technology at scale.
Heath Matlock shared META II: A Syntax-Oriented Compiler Writing Language, by D. V. Schorre from UCLA’s Computing Faculty.
META II is a compiler writing language which consists of syntax equations resembling Backus normal form and into which instructions to output assembly language commands are inserted. […] Each syntax equation is translated into a recursive subroutine which tests the input string for a particular phrase structure, and deletes it if found. Backup is avoided by the extensive use of factoring in the syntax equations. For each source language, an interpreter is written and programs are compiled into that interpretive language.
Interestingly, you can hear more about this paper in a recent Interview between Joe Armstrong and Alan Kay. Alan Kay says this is one of his favorite papers, and Joe says that he lost a month of his life to it, and loved it.
I found a GitHub repo with his metacompiler code in it. Also, here’s a tutorial for writing compilers that goes into some practical detail. Finally, there’s an article about it on Wikipedia.
Fred Yankowski shares a paper, Information distribution aspects of design methodology, from David Parnas.
The role of documentation in the design and implementation of complex systems is explored, resulting in suggestions in sharp contrast with current practice. The concept of system structure is studied by examining the meaning of the phrase “connections between modules”. It is shown that several system design goals (each suggesting a partial time ordering of the decisions) may be inconsistent. Some properties of programmers are discussed. System documentation, which makes all information accessible to anyone working on the project, is discussed. The thesis that such information “broadcasting” is harmful, that it is helpful if most system information is hidden from most programmers, is supported by use of the above mentioned considerations as well as by examples. An information hiding technique of documentation is exhibited in the appendix.
Here’s the abstract:
Programming languages often include specialized syntax for common datatypes (e.g. lists) and some also build in support for specific specialized datatypes (e.g. regular expressions), but user-defined types must use general purpose syntax. Frustration with this causes developers to use strings, rather than structured data, with alarming frequency, leading to correctness, performance, security, and usability issues. Allowing library providers to modularly extend a language with new syntax could help address these issues. Unfortunately, prior mechanisms either limit expressiveness or are not safely composable: individually unambiguous extensions can still cause ambiguities when used together. We introduce type-specific languages (TSLs): logic associated with a type that determines how the bodies of generic literals, able to contain arbitrary syntax, are parsed and elaborated, hygienically. The TSL for a type is invoked only when a literal appears where a term of that type is expected, guaranteeing noninterference. We give evidence supporting the applicability of this approach and formally specify it with a bidirectionally typed elaboration semantics for the Wyvern programming language.
You can download the paper here.