November | 2016 | No Man Steps Twice On The Same Landmine

Cynbe’s life work was the programming language Mythryl. There will be a lot more about Mythryl in future; for now, in honour of his passing, here’s an excerpt from the Mythryl documentation.
________________________________________________________________

In the introductory material I state

Mythryl is not just a bag of features like most programming languages;
It has a design with provably good properties.

Many readers have been baffled by this statement. This is understandable enough; like the first biologists examining a platypus and pronouncing it a fake, the typical contemporary programmer has never before encountered an engineered progamming language and is inclined to doubt that such a thing truly exists, that one is technically possible, or indeed what it might even mean to engineer a programming language. Could designing a programming language possibly involve anything beyond sketching a set of features in English and telling compiler writers to go forth and implement? If so, what?

My goal in this section is to show that it is not only meaningful but in fact both possible and worthwhile to truly engineer a programming language.

Every engineering discipline was once an art done by seat of the pants intuition.

The earliest bridges were likely just trees felled across streams. If the log looked strong enough to bear the load, good enough. If not, somebody got wet. Big deal.

Over time bridges got bigger and more ambitious and the cost of failure correspondingly larger. Everyone has seen the film of Galloping Gertie, the Tacoma Narrows bridge, being shaken apart by a wind-excited resonant vibration. The longest suspension bridges today have central spans of up to two kilometers; nobody would dream of building them based on nothing more than “looks strong enough to me”.

We’ve all seen films of early airplanes disintegrating on their first take-off attempt. This was a direct consequence of seat of the pants design in the absence of any established engineering framework.

The true contribution of the Wright brothers was not that they built the first working airplane, but rather than they laid the foundations of modern aeronautical engineering through years of research and development. With the appropriate engineering tools in hand, building the aircraft itself was a relatively simple exercise. The Wright Flyer was the first controllable, workable airplane because the Wright brothers did their homework while everyone else was just throwing sticks, cloth and wire together and hoping. Sometimes hoping just isn’t enough.

Large commercial aircraft today weigh hundreds of tons and carry hundreds of passengers; nobody would dream of building one without first conducting thorough engineering analysis to ensure that the airframe will withstand the stresses placed upon it. Airplanes no longer fall out of the sky due to simple inadequacy of airframe design.

Airplanes do however fall out of the sky due to inadequacy of flight software design. Software today is still an art rather than an engineering discipline. It ships when it looks “good enough”. Which means it often is not good enough — and people die.

Modern bridges stand up, and modern airplanes stay in the sky, because we now have a good understanding of the load bearing capacity of materials like steel and aluminum, of their typical failure modes, and of how to compute the load bearing capacity of engineered structures based upon that understanding.

If we are to reach the point where airliners full of passengers no longer fall out of the sky due to software faults, we need to have a similarly thorough understanding of software systems.

Modern software depends first and foremost on the compiler. What steel and concrete are to bridge design, and what aluminum and carbon composites are to airframe design, compilers are to software design. If we do not understand the load bearing limits of steel or aluminum we have no hope of building consistently reliable brdiges or airframes. So long as we do not understand what our compilers are doing, we have no hope of building consistently reliable software systems, and people will continue to die every year due to simple, preventable software faults in everything from radiological control software to flight control software to nuclear reactor control software to car control software.

Our minimal need is to know what meaning a compiler assigns to a given program. So long as we have no way of agreeing on the meaning of our programs, as software engineers we have lost the battle before the first shot is fired. Only when we know the precise semantics assigned to a given program by our compiler can we begin to develop methodologies to validate required properties of our software systems.

I do not speak here of proving a program “correct”. There is no engineering analysis which concludes with “and thus the system is correct”. What we can do is prove particular properties. We can prove that a given program will not attempt to read values from outside its address space. We can prove that a given program will always eventually return to a given abstract state. We can prove that a given program will always respond within one hundred milliseconds. We can prove that a given program will never enter a diverging oscillation. We can prove that a given program will never read from a file descriptor before opening it and will always eventually close that file descriptor. We can prove that certain outputs will always stand in given relationships to corresponding inputs. Given time, tools and effort, we can eventually prove enough properties of a flight control program to give us reasonable confidence in trusting hundreds of lives to it.

Traditional programming language “design” does not address the question of the meaning of the language. In an engineering sense, traditional programming languages are not designed at all. A list of reasonable-sounding features is outlined in English, and the compiler writer then turned loose to try and produce something vaguely corresponding to the text.

The first great advance on this state of affairs came with Algol 60, which for the first time defined clearly and precisely the supported syntax of the language. It was then possible for language designers and compiler writers to agree on which programs the compiler should accept and which it should reject, and to develop tools such as YACC which automate significant parts of the compiler construction task, dramatically reducing the software fault frequency in that part of the compiler. But we still had no engineering-grade way of agreeing on what the programs accepted should actually be expected to do when executed.

The second great advance on this state of affairs came with the 1990 release of The Definition of Standard ML, which specified formally and precisely not only the syntax but also the semantics of a complete usable programming language. Specifying the syntax required a hundred phrase structure rules spread over ten pages. Specifying the semantics required two hundred rules spread over another thirty pages. The entire book ran to barely one hundred pages including introduction, exposition, core material, appendices and index.

As with the Wright brother’s first airplane, the real accomplishment was not the artifact itself, but rather the engineering methodology and analysis underlying it. Languages like Java and C++ never had any real engineering analysis, and it shows. For example, the typechecking problem is for both of those languages undecidable, which is mathematical jargon for saying that the type system is so broken that it is mathematically impossible to produce an entirely correct compiler for either of them. This is not a property one likes in a programming language, and it is not one intended by the designers of either language; it is a simple consequence of the fact that the designed of neither language had available to them an engineering methodology up to the task of testing for and eliminating such problems. Like the designers of the earliest airplanes, they were forced to simply glue stuff together and pray for it to somehow work.

The actual engineering analysis conducted for SML is only hinted at in the Defintion. To gain any real appreciation for it, one must read the companion volume Commentary on Standard ML.

Examples of engineering goals set and met by the designs of SML include:

Each valid program accepted by the language definition (and thus eventually compiler) should have a clearly defined meaning. In Robin Milner’s famous phrase, “Well typed programs can’t go wrong.” No segfaults, no coredumps, no weird clobbered-stack behavior.

Each expression and program must have a uniquely defined type. In mathematical terminlogy, the type system should define a unique most general principal type to each syntactically valid expression and program.

It must be possible in principle to compute that type. In mathematical terminology, the problem of computing the principal type for an expression or program must be decidable. This is where Java and C++ fall down.

In general it is excruciatingly easy for the typechecking problem to become undecidable because one is always stretching the type system to accept as many valid expressions as possible.

Any practical type system must err on the side of safety, of rejecting any program which is not provably typesafe, and will consequently wind up throwing out some babies with the bathwater, rejecting programs which are in fact correct because the type system was not sophisticated enough to realize their correctness. One is always trying to minimize the number of such spuriously rejected by being just a little more accomodating, and in the process creeping ever closer to the precipice of undecidability. The job of the programming language type system designer is to teeter on the very brink of that precipice without ever actually falling over it.

It must be possible in practice to compute that type with acceptable efficiency. In modern praxis that means using syntax-directed unification-driven analysis to compute principal types in time essentially linear in program size. (Hindley-Milner-Damas type inference.)

There must be a clear phase separation between compile-time and run-time semantics — in essence, between typechecking and code generation on the one hand and runtime execution on the other. Only then is it possible to write compilers that generate efficient code, and only then is it possible to give strong compile-time guarantees of typesafety.

The type system must be sound: The actual value computed at runtime (i.e., specified by the dynamic semantics must always possess the type assigned to it by the compiletime typechecker (i.e., static semantics.

The runtime semantics must be complete, assigning a value to every program accepted as valid by the compiletime typechecker.

The design process for SML involved explicitly verifying these properties by informal and formal proofs, repeatedly modifying the design as necessary until these properties could be proved. This intensive analysis and revision process yielded a number of direct and indirect benefits, some obvious, some less so:

Both the compiletime and runtime semantics of SML are precise and complete. there are no direct or indirect conflicting requirements, nor are there overlooked corners where the semantics is unspecified.
This sort of analysis is arduous and lies at the very limits of what is possible at the current state of the art. Consequently there was a powerful and continuing incentive to keep the language design as spare and clean as humanly possible. The original 1990 design was already very clean; the 1997 revision made it even simpler and cleaner by removing features which had since been found to be needlessly complex.
The analysis explicitly or implicitly explored all possible interactions between the different language parts; each was revised until it interacted smoothly with all other parts in all possible contexts. It was this process which took an initial bag of features and welded them into a coherent design. It is the lack of this process which has left other contemporary languages still an uncoordinated bag of features rife with unanticipated corner cases.
The analysis process exposed initially unanticipated design consequences and concomitant design choices, allowing explicit consideration of those design choices and selection of the most promising choice. Other contemporary languages have discovered these design consequences only in the field when the size of the installed base prevented a design change. For example it was not initially anticipated that every assignment into a Java array would require a type check; this unexpected cost will handicap Java forever. The undecidability of Java and C++ typechecking are similar unexpected and unpleasant design misfeatures discovered too late to be correctable.
The analysis process made clear which language features were semantically clean and which introduced pervasive semantic complexities. For example:
The original Definition handling of equality introduced special cases throughout the semantic rules and proofs; more recent research such as the Harper Stone semantics for the language have addressed this by finding a simpler, more natural treatment.
The original Definition treatment of type generativity was via an imperative-flavored mechanism which proved resistant to analysis; the more recent Harper Stone semantics has addressed this via a clean type-theoretic treatment more amenable to analysis.
The original Definition reconciliation of type polymorphism with the imperative features of assignment and exceptions proved needlessly complex; the 1997 revision adopted the simplified “value restriction” approach now universally adopted in ML-class languages.
The analysis process identified problematic areas in which the semantic consequences of particular features was not clearly understood; these features were left out of the design, forestalling possible unpleasant discoveries later. For example, inclusion of higher order functors was postponed pending deeper understanding of them.
Conversely, the analysis identified some generalizations of the language as being in fact unproblematic, allowing certain language features which initially looked suspect to be included in the language, either in the Standard itself or in commmon extensions.

SML was the first general-purpose realistic programming language to enjoy rigorous engineering-grade design analysis of this sort comparable to what we routinely do for a proposed bridge or airframe. SML/NJ is the reference implementation of SML, constructed with the active assistance of the SML language designers. Mythryl inherits this theoretical foundation and this codebase, and adapts it to production use in the open source tradition.

No Man Steps Twice On The Same Landmine

Monthly Archives: November 2016

Why Mythryl?

Sandy, Cynbe, and Friends' Brainfarts (experimental)