Re: Layout syntax

Hans Aberg wrote:


> The question is what happens when math is written proof verification
> system, as the computer can easily check any nesting: then manual
> unnesting will no longer needed. So one will probably see more of
> such nesting then.


I don't think that this would be a Good Thing.
After all, proofs aren't just read by computers, they are also read by
humans (e.g. to check whether a proof states what was intended, or to
modify a proof to prove something slightly different but more
interesting), and humans don't parse nested constructs very well.


> I certainly admit nesting in my proof verification system: It is
> declarative, and one can have local variables, just as in say C/C++
> and most other modern declarative languages.


It's good to allow nesting. Two or three levels of nesting are usually
easily parsed by a human. It's just that nesting shouldn't go to
arbitrary levels. I routinely remove deeply-nested construct and put
them into separate, named constructs and then just use the name. (Just
as mathematicians are told to do.)


>> That's exactly my point: mathematical syntax, designed for
>> consumption by humans, isn't easily transferable to computer
>> language syntax, designed for consumption by computers. In other
>> words, drawing syntactical inspiration from actual mathematical
>> usage may be helpful, but sooner or later one is going to run into
>> trouble.
>
> My development strategy is to wrestle a bit with the more common
> popular syntactic features, such as sets, function definitions and
> the like, to make them close to actual mathematical usage. Then, if I
> get so far, added user math should use a less complicated syntax,
> perhaps defined by some operator precedence.


Seems reasonable.


>> Which is just my point: mathematics isn't the best source of
>> inspiration when it comes to syntax. (It's an excellent source of
>> inspiration when considering semantics! At least if a precise
>> semantics is desired.)
>
> Quite on the contrary: Just because of these difficulties, math
> becomes an important source if inspiration, because these apparent
> syntactic quirks are in reality there so as to produce a syntax that
> is efficient to humans. So, as computer languages can, in view of
> better computers, become more adapted to humans, it is important to
> have this input.


I think we're largely in agreement, and just differ in how far one
should go when trying to import mathematical conventions into a
computerized language.
I.e. I agree that arithmetic operators should be in any language, I'm
not so sure about difficult-to-parse constructs like lambdas without a
lambda keyword (but it might be worth the effort if the language is
specifically tailored towards expressing traditional math), and I
wouldn't even consider mimicking tabular layout to represent matrices
(but that's just me - if conformance to mathematical conventions is
important enough, it might be important enough to at least give it a stab).


Regards,
Jo

Return to the comp.compilers page.
Search the comp.compilers archives again.