Axiomatic LanguageΒΆ
Authors: | Walter Wilson |
---|---|
Time: | 14:15 |
Session: | https://thestrangeloop.com/sessions/axiomatic-language |
Link: | http://axiomaticlanguage.org/ |
Slides: |
Axiomatic has four goals:
- Pure specification – what, not how
- Minimal but extensible – as small as possible
- Metalanguage – able to imitate other languages
- Beautiful
Speificiation by Enumeration: a program can be specific by an infinite set of symbolic epxressions that enumerate all possible inputs or sequences of inputs along with the corresponding outputs. Additionally, you could create a syntax for describing programs in terms of the input and output files. But what about interactive programs? This is a specialization of the previous case: instead of a single input specification and a single output specification, the enumeration interleaves input and output, again exhausitvely.
If you accept the premise that this enumeration is a specification, then what you need is a way to formally describe the enumerations. Axiomatic syntax supports atoms, expressions, strings, and sequences. The axiom construct is a conclusion (output) and some set of conditions. In the core language, the program generates expressions if all the conditions of an axiom instances are valid (true).