contact:
    Walter W. Wilson
    wwwilson at acm dot org

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).
  ((%) $ $)< (% $).

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

Phonecode in Axiomatic Language - a paper for ICLP 2024
Phonecode in 8 lines! - webpage
utilities: form.ax, ho.ax, natnum.ax, bit.ax, char.ax, bool.ax. stream.ax.

Definition of ASP in axiomatic language
utilities: form.ax, ho.ax, bit.ax, char.ax, bool.ax.

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.

some example programs