Emerging Languages Camp Part 5: Axiomatic Language
This is the fifth post of my notes from Emerging Languages Camp last year. If you haven’t seen it already, you might want to read the Introduction to this series.
Homepage · Slides · Presentation
One of the ways that you can describe a coding style is declarative versus imperative. That is, focusing on the desired result versus focusing on how that result should be computed, respectively. Walter Wilson's axiomatic language attempts to take the former approach as far as possible. It is a pure specification language which attempts to provide a means for exhaustively specifying the output of a program. As such, it is more comparable with specification languages like TLA+ than with programming languages designed around the idea of producing an executable.
If you can specify every property or every possible input and output desired from a system, then you might be able to write a program which could read that specification and produce a program which implements it. In fact, dependently typed languages like Agda can do this today in a more limited capacity.
Actually building such a working system, Walter concedes, is a challenge! I'll talk more about that challenge in a moment, but first let's take a look at what he has actually built. I am not aware that there is any working software here; at this point, the project is just the grammar. The semantics include axioms and expressions. Axioms generate valid expressions. The syntax includes four elements:
Now you can use these to build axioms, with the following syntax:
Axioms produce axiom instances, where values are substituted for the axiom variables. Axiom instances produce valid expressions. If the conditions of an axiom instance are valid expressions, then the conclusion is a valid expression. The examples are somewhat lengthy, so I will refer you to the axiomatic language homepage, which includes many sample programs.
This was a very thought-provoking presentation. When I listened to many of the other speakers, I often had mental reactions like, "Hey, that's a really useful thing!" or "That's not my cup of tea." When I listened to Walter's presentation, however, my reactions were more along the lines of, "Is this even possible?" and "If so, is it a good idea?" (In a good way!) I really don't know the answers. When I spoke with Walter later, thanking him for making me think, he asked me if I thought that an implementation of such a system would be possible. My gut reaction is that, much like termination analysis, the general answer is no, but it might be possible to handle enough specific, useful cases to produce a usable system anyway.
Axiomatic language is clearly useful as an intellectual exercise. Would it also be useful as a practical system? As an industry, I don't think we know very much about writing great specs. My gut feel is that it is harder to write a spec which is so complete that it can be used to produce a functional system than it is to write correct code. It is usually harder to work at a higher level of abstraction, though it's often worth the effort!
Although Walter claims that specifications are "smaller & more readable than algorithms," my conclusion is not so clear-cut. Compare this sort in Haskell with Walter's specification for a sort in axiomatic language. In general, when I look at Walter's examples, I think it is fair to say that the claim that the specifications would be smaller and more readable than algorithms is, at best, debatable. Very expressive code in a contemporary, high level language, in my opinion, can do better, without introducing too much inessential imperative overhead. You can also compare Walter's natural number addition from his slide deck with this example in Agda. The advantage of a specification over an implementation, I think, is that specifications can be free of implementation details.
These examples are not a perfect comparison. I would point out that the axiomatic language sort specification there is incomplete because it does not specify performance or space boundaries. Also, the Haskell version does not specify ordering relations, but Walter's example does. Nevertheless, when I read the Haskell version I can clearly see what is going on, both in terms of what the result will be and I have some idea of the amount of time it will take. I can see the result fairly clearly in Walter's version, but it takes a good bit more reading. And I have no idea how long it will take.
Actually, I don't even know how long the sort should take, because that probably depends upon the application. A more complete specification might include information about the expected length of the input and an upper bound on time, available memory, etc. But such details, while important, bring us dangerously close to specifying an algorithm, which is exactly what Walter is trying to avoid!
For more complicated, but still realistic, problem domains ("I need a program which will calculate the correct income tax for any US citizen."), I rather doubt that a complete specification, sufficient to produce a working program, is even possible. The US tax code, vague in some places and self-contradictory in others, certainly would not provide enough information to do such a thing. However, it would still be useful if you were able to somehow translate the US tax code into a machine-readable specification, in order to test the program you produced by other means. There may be subsets of the tax code which are deterministic and it's probably useful to verify implementations of these via machine-assisted proof.
One might at first be tempted to confuse programming via specification with waterfall, but these methodologies are orthogonal, I think. You can develop a specification in an agile manner, just like you can do waterfall without a formal specification.
Axiomatic language also reminds me of the philosophical languages of the 17th century, which attempted to produce minimal, concise grammars in which it was impossible to make an incorrect statement. Where axiomatic language differs from all of these is the as yet unfulfilled intention of enabling a system by which a program can be automatically generated (as opposed to "merely" checking satisfiability).
In the next post in this series I’ll discuss Matt Graham’s qbert bytecode.
Axiomatic Language
Walter Wilson
Homepage · Slides · Presentation
One of the ways that you can describe a coding style is declarative versus imperative. That is, focusing on the desired result versus focusing on how that result should be computed, respectively. Walter Wilson's axiomatic language attempts to take the former approach as far as possible. It is a pure specification language which attempts to provide a means for exhaustively specifying the output of a program. As such, it is more comparable with specification languages like TLA+ than with programming languages designed around the idea of producing an executable.
If you can specify every property or every possible input and output desired from a system, then you might be able to write a program which could read that specification and produce a program which implements it. In fact, dependently typed languages like Agda can do this today in a more limited capacity.
Actually building such a working system, Walter concedes, is a challenge! I'll talk more about that challenge in a moment, but first let's take a look at what he has actually built. I am not aware that there is any working software here; at this point, the project is just the grammar. The semantics include axioms and expressions. Axioms generate valid expressions. The syntax includes four elements:
- Atoms: `abc, `+
- Expression variables: %w, %3
- String variables: $, $xyz
- Sequences:(), (`M %x (`a $2))
Now you can use these to build axioms, with the following syntax:
<conclu> < <cond1>, …, <condn>.
<conclu>. ! an unconditional axiom
Axioms produce axiom instances, where values are substituted for the axiom variables. Axiom instances produce valid expressions. If the conditions of an axiom instance are valid expressions, then the conclusion is a valid expression. The examples are somewhat lengthy, so I will refer you to the axiomatic language homepage, which includes many sample programs.
This was a very thought-provoking presentation. When I listened to many of the other speakers, I often had mental reactions like, "Hey, that's a really useful thing!" or "That's not my cup of tea." When I listened to Walter's presentation, however, my reactions were more along the lines of, "Is this even possible?" and "If so, is it a good idea?" (In a good way!) I really don't know the answers. When I spoke with Walter later, thanking him for making me think, he asked me if I thought that an implementation of such a system would be possible. My gut reaction is that, much like termination analysis, the general answer is no, but it might be possible to handle enough specific, useful cases to produce a usable system anyway.
Axiomatic language is clearly useful as an intellectual exercise. Would it also be useful as a practical system? As an industry, I don't think we know very much about writing great specs. My gut feel is that it is harder to write a spec which is so complete that it can be used to produce a functional system than it is to write correct code. It is usually harder to work at a higher level of abstraction, though it's often worth the effort!
Although Walter claims that specifications are "smaller & more readable than algorithms," my conclusion is not so clear-cut. Compare this sort in Haskell with Walter's specification for a sort in axiomatic language. In general, when I look at Walter's examples, I think it is fair to say that the claim that the specifications would be smaller and more readable than algorithms is, at best, debatable. Very expressive code in a contemporary, high level language, in my opinion, can do better, without introducing too much inessential imperative overhead. You can also compare Walter's natural number addition from his slide deck with this example in Agda. The advantage of a specification over an implementation, I think, is that specifications can be free of implementation details.
These examples are not a perfect comparison. I would point out that the axiomatic language sort specification there is incomplete because it does not specify performance or space boundaries. Also, the Haskell version does not specify ordering relations, but Walter's example does. Nevertheless, when I read the Haskell version I can clearly see what is going on, both in terms of what the result will be and I have some idea of the amount of time it will take. I can see the result fairly clearly in Walter's version, but it takes a good bit more reading. And I have no idea how long it will take.
Actually, I don't even know how long the sort should take, because that probably depends upon the application. A more complete specification might include information about the expected length of the input and an upper bound on time, available memory, etc. But such details, while important, bring us dangerously close to specifying an algorithm, which is exactly what Walter is trying to avoid!
For more complicated, but still realistic, problem domains ("I need a program which will calculate the correct income tax for any US citizen."), I rather doubt that a complete specification, sufficient to produce a working program, is even possible. The US tax code, vague in some places and self-contradictory in others, certainly would not provide enough information to do such a thing. However, it would still be useful if you were able to somehow translate the US tax code into a machine-readable specification, in order to test the program you produced by other means. There may be subsets of the tax code which are deterministic and it's probably useful to verify implementations of these via machine-assisted proof.
One might at first be tempted to confuse programming via specification with waterfall, but these methodologies are orthogonal, I think. You can develop a specification in an agile manner, just like you can do waterfall without a formal specification.
Axiomatic language also reminds me of the philosophical languages of the 17th century, which attempted to produce minimal, concise grammars in which it was impossible to make an incorrect statement. Where axiomatic language differs from all of these is the as yet unfulfilled intention of enabling a system by which a program can be automatically generated (as opposed to "merely" checking satisfiability).
Up Next
In the next post in this series I’ll discuss Matt Graham’s qbert bytecode.
Tags:
Agda
axiomatic language
Conference Papers
General Software Development
specification
TLA+
Walter Wilson
Craig, thank you for writing about axiomatic language!
As for specification size, the Haskell quicksort example makes use of Haskell's built-in features for function definition, lists, ordering relations, and the filter higher-order function. Axiomatic language, on the other hand, is extremely minimal and has none of these features built-in. My sorting specification example thus had to define characters, ordering, and other utility functions. Ultimately these would be provided in a standard library and would not be counted as part of the lines of code for an application.
As for sorting performance, the "grand challenge" of axiomatic language implementation is to create a system that can "understand" the sorting axioms and then generate an efficient sorting program. Ideally, the use should have confidence that the specification would be well-implemented. Performance would not be part of the specification.