Axiomatic Language

A minimal pure-specification logic programming language
with meta-language capability.

InfoQ Video - 2013 Emerging Languages Camp

Axiomatic Language Theme Song
(other music: Giga and William Tell Overture)

contact:
Walter W. Wilson
wwwilson at acm dot org

Overview of Axiomatic Language
(pdf)

Axiomatic language is proposed as a tool for greater programmer productivity and software reliability.

Goals — Axiomatic language has the following goals: (1) pure specification – you tell the computer what to do without telling it how to do it, (2) minimal, but extensible – as small as possible without sacrificing expressiveness, (3) a metalanguage – able to incorporate the capabilities and advantages of other languages, and (4) beauty.

Idea — Axiomatic language is based on the idea that the external behavior of a function or program – even an interactive program – can be represented by a static, infinite set of symbolic expressions. These expressions enumerate inputs – or sequences of inputs – along with the corresponding outputs. For an interactive program each expression would record the inputs/outputs of a particular execution history as seen by an external observer. The set of expressions would cover all possible execution histories. The language is just a formal system for defining these infinite sets.

Recipe — Axiomatic language can be described as pure, definite Prolog with Lisp syntax, HiLog higher-order generalization, and “string variables”, which match a string of expressions in a sequence. (See details at this webpage or this paper.)

Example — In axiomatic language a finite set of “axioms” generates a (usually) infinite set of “valid expressions”. For example, the following two axioms,

```  (a b).
((%) \$ \$)< (% \$).
```
generate the valid expressions (a b), ((a) b b), (((a)) b b b b), etc. The symbols % and \$ are expression and string variables, respectively.

Benefits — Specifications should be smaller and more readable than algorithms. (Specifications just define external behavior while implementation code defines both external behavior and internal processing.) Specification definitions should also be more reusable than code constrained by efficiency. Thus, smaller code size should provide increased programmer productivity.

The purity and small size of axiomatic language should make it well-suited to proof. Proof would guarantee equivalence between the user's specification and the generated program. One may also be able to prove assertions about specifications to validate them and this could be more powerful than just testing.

Implementation Challenge — The problem of automatically transforming specifications to efficient programs can be considered a grand challenge of computer science. If the target is a parallel machine, it subsumes the problem of automatic parallelization. This transformation problem is a form of the old automatic programming problem, except that here we are not trying to understand natural language requirements and the system is not expected to have knowledge about any particular application domain. Also, the specifications are complete – the system doesn't have to infer an input/output function from examples.

In summary, axiomatic language can be seen as idealistic in its goals, intriguing in its potential, and formidable in its realization.

Papers & links on axiomatic language:

A Foundation for the DoD Digital Transformation: Proposal, Response. (approved for release)

A More General Specification Language, Workshop on Progress Towards the Holy Grail
at ICLP 2017, Melbourne, Australia, August 28, 2017, slides
SEND_MORE.txt - SEND+MORE=MONEY problem
Sudoku.txt - Sudoku program
blend.txt - optimal blending of ingredients
util/natnum.txt - utility predicates for natural numbers
util/ho.txt - higher-order predicates
util/form.txt - utilities involving expression form
util/relation.txt - relational operators
util/eval.txt - evaluation of decimal number expressions

Video! Presentation at Polyglot Programming DC, Washington, D.C., Dec. 2, 2015, slides

Video! Presentation at the 2013 Emerging Languages Camp at Strange Loop
slides, Calculator Program, procedural language definition, utilities

A Tiny Specification Metalanguage, SEKE 2012, slides. ( Proceedings (54MB)).

Extended Axiomatic Language – using the complement of a valid expression set for specification

Specifying Input/Output by Enumeration, PLDI 2010 FIT: Fun Ideas and Thoughts (blog).

A Long-Term Logic Programming Language, ALP Newsletter, May 2004.

A Minimal Specification Language, LOPSTR 2000 Pre-Proceedings (slides).

Beyond PROLOG: Software Specification by Grammar, SIGPLAN Notices, Sept. 1982, pp.34-43.

Application of axiomatic language to engineering design:

A Vision for CAD , Lockheed Martin -- approved for public release

Thoughts on LOTAR -- LOng Term Archiving and Retrieval.

A Language for Engineering Design, 2007 NASA-ESA Workshop on Product Data Exchange.

Miscellaneous -- Nothing to do with axiomatic language:
Complaint about MedStar Data Breach Settlement