Eidola semantics

Eidola Semantics

Semantics? Wuzzat?

A formal semantics maps some problem domain of interest (in our case, a programming language) into some better-understood, more mathematical domain. This aids in the design of the language, provides criteria for implementations, allows formal verification of the language and programs written in it, and other such good things.

Eidola's semantics also holds an unusual central role. Since Eidola is representation-independent, the semantics not only represents the language, but actually is the language---implementations represent the semantics instead of the reverse. What a wild thought!

You can learn more in the semantics reference, and in a soon-to-be-written fascinating treatise on the reasoning behind the semantics.

Status

What's done: I have a young but solid form of the static (i.e. non-runtime) semantics for named elements (packages, classes, variable and functions). Read and enjoy! Several unresolved questions have surfaced, and need your input.

Current work: It's time to start describing what's inside a function. I'll begin with begin with local variables, class member access, function calls, and assignments. Developing the algorithmic, scoping, and runtime semantics for these few constructs will actually cover most of the major big holes remaining in the semantics. The section on scoping is in an early draft form, and needs a lot of work. It will iron out as the algorithmic semantics take shape.

Coming soon: The current document on the semantics is really intended as a reference document -- it tells what is part of Eidola, but not why. I would eventually like to explain some of the reasoning behind them, which will include a good deal of pontificating on object-oriented philosophy. This is currently taking a back seat to implementation and a desire to get started on notation, but I swear it will happen.

In the future: It would be interesting to study at some point the mathematical properties of the semantics, such as proving its consistency, or drawing illuminating correspondences between the semantics and algebraic structures like groups and categories.