What is Expressiveness in a Computer Language

[Stephen J. Bevan]

Darren New <dnew at san.rr.com> writes:
> Andreas Rossberg wrote:
>> AFAICT, ADT describes a type whose values can only be accessed by a
>> certain fixed set of operations.
>
> No. AFAIU, an ADT defines the type based on the operations. The stack
> holding the integers 1 and 2 is the value (push(2, push(1,
> empty()))). There's no "internal" representation. The values and
> operations are defined by preconditions and postconditions.

As a user of the ADT you get a specification consisting of a signature
(names the operations and defines their arity and type of each
argument) and axioms which define the behaviour of the operations.

The implementer has the task for producing an implementation (or
"model" to use alebraic specifiction terminology) that satisfies the
specification.  One model that comes for free is the term model where
the operations are treated as terms and the representation of a stack
containing 2 and 1 would just be "(push(2, push(1, empty())))".
However, while that model comes for free it isn't necessarily the most
efficient model.  Thus the non-free aspect of chosing a different
implementation is that technically it requires an accompanying proof
that the implementation satisfies the specification.