**Axiomatic Language
**

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

**
YouTube Video - Dec. 2, 2015 Polyglot Programming DC
**

**
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

(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.

Proof Checker for Axiomatic Language,

Axiomatic Language and Proof
draft paper

Proof in Axiomatic Language

Proof of Reverse Specification/Implementation Equivalance

proofs about even/odd natural numbers

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

Proof, Implementation, and CAD-Application
Challenges of Axiomatic Language,

36th Intl. Conf. on Logic Programming (ICLP 2020)
Research Challenges Track

slides,
video

Axiomatic Language: A Short Presentation (slides),

talk at
35th Intl. Conf. on Logic Programming (ICLP 2019)

A Language for Ultra-Long-Term CAD Data Preservation (slides),

talk at
SIAM Conf. on Computational Geometric Design (GD19)

Baby Steps Toward an Implementation of Axiomatic Language

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

Screencast submission to the Future Programming Workshop at SPLASH 2014.

Submissions to
DARPA Grand Challenges of the 21st Century:

Automatic Programming Using Axiomatic Language

An Engineering Design Language

ICLP 2011
Doctoral Consortium
submission: Implementation of Axiomatic Language,
slides.

(Proceedings,
DOI)

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.

(ACM link)

**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.