The TUNES HLL Specifications

General Concepts

Safety and Security Issues

Standard Basic Constructors

Meta-Level Architecture

Standard Syntax

Standard Library of language extensions

This should consist of instances of meta-level architecture components, and uses of these to provide some convenient environment for expressing enough of present-day idioms (such as shell syntax) for the purpose of retaining the conveniences they serve. Gradually these should be incorporated into a larger, regularized framework.


Implementing Annotations

Keeping Proofs Tractable

To merge:


The system must provide as part of language semantics access to a choice axiom concept, similar to the epsilon calculus. We explain this choice axiom:

One way to understand programming with epsilons (Epsilon stands for Hilbert's epsilon symbol for a witness for an existential predicate) is to view them as goals in the classical paradigm of higher-order logic programming (see languages like Prolog, Mercury, Lambda Prolog, Goedel, Maude); an epsilon is a hole in the well-founded construction of a computable object; the system thus uses tactics to fill the hole; these tactics are made of rules that may include holes themselves, hence generating filling of the subholes as subgoals.

The main differences of Tunes epsilon calculus with classical logic programming is that tactics can be dynamically defined from existing tactic constructs and libraries, and they are first-class objects, themselves subject to manipulation, etc. Also, there is a guaranteed constraint that should they succeed, they should return an object that rigorously matches the requested specification; hence, whereas Prolog programs only have a global semantics that can only be deduced from the totality of rules, Tunes tactics can have a nice local semantics with local definitions.

If O is an object with a free variable e, then O[E/e] where E is a compliant tactic to fill 'hole' e is a valid object and specialization for O. E may dynamically generate holes itself, etc.

The tactics are constrained to return a result that respect the specification for the requested object, instead of being pure arbitrary tactics in a program with global semantics only.

Abstraction & Migration

References considered Harmful

It seems to me that references are not a good concept in a distributed system. Communication Channels, Linear objects, and projects seem to do more than references, in more precise ways:

To Do: