Re: Verified compilers?

[Georg Bauhaus <rm.dash-bauhaus@futureapps.de>]

On 10.03.12 21:35, Niklas Holsti wrote:
> One should use the simplest formalism that is powerful enough for one's needs. You probably don't consider grammars and parsing tools simple, but that is a matter of opinion and personal taste.


Simplicity, if I may throw in a remark for later discussion, is
frequently said to be an important property of a formalism.  Opinion
or taste may not adequately reflect the importance.  More adequacy
can be achieved through observation.

Simplicity can be defined to be not just a matter of opinion, or of
taste. It is a tuple, then, having two components at least:

   (simplicity felt, simplicity measured).

The components correspond, roughly, to subjective and objective.
Nailing these components down proceeds as follows.

1. Subjective simplicity:

Subjects can declare the simplicity of a thing T on a subjective scale
when stating their opinion. We can observe them saying, "It's simple!"
This is the first, the subjective component of the tuple.  (Validity of
the data might be spoiled by affection or loyalty, etc., but this can be
checked.)

2. Objective simplicity:

To learn about simplicity of a thing T, observe the degree to which
subjects solve a given problem P, employing thing T.  Have two groups
of subjects solve P, one employing T and the other employing T'.
Then, a thing T is objectively simpler than a different thing T' if
the T-group is more effective at solving P. "More effective" can refer
to time needed, and to steps done.

(As usual, the groups would have to be comparable. E.g., subjects in
either group have the same amount of experience using T and T',
respectively.)

An example of subjective simplicity is when someone highly skilled in
game theory says, "Rubik's cube is simple to solve!". Not everyone
agrees. Objectively, Rubik's cube seems not so simple.