Re: an extension of the mizar language for dealing with article metadata
Josef Urban <[email protected]>
| Newsgroups | gmane.comp.mathematics.mizar |
|---|---|
| Message-ID | <[email protected]> |
On Sun, 30 Nov 2008, trybulec wrote: > Josef Urban wrote: > >> >> So why is the keyword "begin" allowed multiple times to introduce sections, >> and why do all articles start with the standard header containing author >> and title, why are comments allowed at all? If there is no need to process >> and present these article > > That is my complaint, the repetition of 'begin' has nothing to do with Mizar, > and should not be allowed. I would prefer > something like: > > ::$ SECTION > > maybe with a name, as a cross reference to the place where description of the > section is kept: > the title, maybe a summary > > BTW. In Mizar HPF (around 1993) only one kind of comments was allowed: > written by a pen on the printout. > It did not work. No wonder. http://en.wikipedia.org/wiki/Literate_programming Comments in programming languages serve as a general storage for anything that the language does not capture yet. If there is a frequent need for expressing certain annotations, such annotations should be eventually made more formal and taken care of by extending the language's syntax. I think Isabelle/Isar has done this, and the result is that it is much easier to write publishable papers about Isar formalizations (or more precisely: the formalizations can already contain all the TeX documentation/paper). Josef