One of these people, Nick Weininger, who helped build a real-time avionics operating system, wrote a really marvelous paper on what kind of work this involved, and how a language like Eidola could help make such work faster and cheaper. On this page, he helps briefly restate of some of his thoughts on how a mission-critical developer might use Eidola.

This is a problem Eidola can address, and not only because of the potential of better notation to make code more understandable. Because an Eidola program is interactive at edit time, a reviewer can interrogate it to understand the program's structure, and check this structure against the specification. The more independent the reviewer is, the more important this capability becomes.

Suppose you are assigned to review part of a program that you've never seen before. For example, you might be asked to ensure that the Foobar class performs, and is used by other classes, in a manner matching its specification. If you've ever actually had to do something like this, you know that it can be close to an impossible task. You might end up with a nicely filled-out review checklist with all the i's dotted and t's crossed, but it is unlikely you will be able to do a real and thorough examination of the class's correctness.

Why? Well, consider what you have to do to perform such an examination. If you're reviewing good code on a well-organized project, the header file for the Foobar class will contain a well-written, clear explanation of what the requirements on the class are; the headers for each function will explain what the function does, what the conditions are on its arguments, etc. So far, so good. (I can hear most of you snickering already).

But this is only the beginning. One requirement might say that the Foobar class fits into the GiantEventQueue in a certain way. What's the GiantEventQueue? Call up another file, read another explanation, try to grok all the author's references to six other classes. Another requirement might say that the Foobar::SelfDestruct() method must only be called after the global initialization of the Frammitz class. Now you have to search through all the places where the SelfDestruct() is called, look for the Frammitz initializations before those calls, worry about whether you missed one because of some subtlety of program flow....

At this point, you Emacs studs out there are probably still unconcerned. "What's the problem?" you say. "I can write an elisp macro in five seconds that will automate all that searching for me." OK, sure, a good programmer's editor could keep you sane so far. But now suppose you come across the requirement:

WARNING: Instances of Foobar may only be added to or removed from other Foobars or FrammitzFinders, and then only if they really like each other. Under no circumstances may a Foobar be added to a WrestlingMarmot or one of its subclasses, as a FatalGiggleException may result.

The essential problem here is the tediousness of understanding the complex semantic structure in which program components are embedded, and the difficulty of searching for constructs based not on their syntax, but on their semantics. Text editors cannot really remedy this problem because they don't understand (or at best, understand only superficially) the semantics of what they're editing.

But an Eidola notation does understand that semantics, so constructing semantically-based search-and-display constructs would be a snap. Want to search for calls to the "add" function where one argument is a Foobar and the other argument has a WrestlingMarmot as its ancestor? No problem. Want to display all of the places where a Foobar is passed to a GiantEventQueue method? Piece of cake. With these sorts of capabilities, a good Eidola notation could alleviate the pain of one of the most thankless, and necessary, tasks in software development.

Although Eidola focuses on semantic structures in a program, it will also allow a notation to attach hints to pieces of code. They might be display hints -- for example, a sequential ordering or a two-dimensional arrangement of the members of a class.

Hints need not be all sugar, however. Structured documentation stored as hints are a way of realizing Donald Knuth's idea of "literate programming", or self-documenting code. In a mission-critical context, hints could carry not only English, but computer-parsable cross-references to a set of specifications. Given a notation that knows how to handle these specification hints, it would be possible to ask "show me the specs that this code implements", or "show me all the code related to this spec", without any tedious human effort. There would, of course, still be tremendous human effort involved in keeping code tied with the appropriate specs, but such work would carry a greater reward in Eidola. Once again, the software can't think for the programmers; it can only help them when they're willing.

A more powerful method is to determine which parts of the code could affect these assertions, then use software which can model the behavior of these parts and check the assertions against the space of all possible software states. When the assertion fails, a good formal modeling tool can graphically display the circumstances leading to the assertion failure, allowing the developer to figure out where the bug came from easily. The problem with currently available formal modeling tools is that the good ones can't work directly on the code itself; they need it to be translated to a modeling language which has an easily manipulable formal semantics.

In a language like Eidola, this translation would be easier, since the fundamental form of programs is already expressed by a formal semantics. Furthermore, the process of "program slicing", extracting the slice of a program related to a particular assertion and boiling that slice down to a form more suitable for modeling, could be at least partially automated. This would save time and dramatically reduce the potential for mistranslation. And such a translation would be much easier to write for Eidola, with APIs already available for dealing with the code's structure, than for a traditional language, which would require writing or adapting a partial compiler for the source code.

Also, a good notation might integrate modeling with the development process, allowing testing to be done more often in the course of development. If you wanted to know whether your nifty new class would work correctly with two existing classes, and you had a rigorous expression of what "correctly" means, the notation could let you select the classes to model, run the modeling tool, and display any errors found in the context of the program code itself-- not in the context of the sliced model.