Re: [mizar] Mizar 7?

[Freek Wiedijk <freek@cs.kun.nl>]

Dear Andrzej,

>There are problems with errors recovery (I suspect that the popularity of
>'interactive' systems is caused by the fact that
>interactivity, which is easy to implement, enables to justify the lack of
>errors recovery, which is difficult).

You raise an interesting point here.

Would you think a version of Mizar that only would report the
_first_ non *4 error and then quit, that it would be much
less usable than the current one?

Dan Synek always claims to me that this whole error recovery
stuff dates from a time when computers were big, slow, and
you had to wait for the result of one run for an hour because
it would come on line printer paper from a mainframe.

I'm not sure what to think of this myself, though.

Freek