Re: [mizar] Errors recovery

[Andrzej Trybulec <trybulec@math.uwb.edu.pl>]

Piotr Rudnicki wrote:

> No matter what are the current politically correct trends in education
> industry, distance learning is pretty useless as attested by its
> results that I see on a daily basis.  Besides, in distance learning as
> widely done in this country, the turnaround time is a few hours rather
> than days.  They use e-mail and web.
>

Notwithstanding your opinion on distant learning, let us talk about regular courses.
To be more realistic:
In the course "Introduction to Logic and Set Theory" we had (Ania Zalewska and me)
in average
8 students in the laboratory. In one teaching session they are supposed to prove 2 -
5 theorems in e.g. theory
of binary relations.
I can work with one student explaining, how to correct an error (and what is the
cause ot the error). It takes let us say 3 minutes. TS lasts 105 minutes, so I have
in average about 12 minutes for a student, so I talk to him app. 4 times.
Of course, I allow students for discussing errors between themselves, and sometimes
I ask for attention and explain the problem for the whole group. Still, if they do
not know how to correct an error, they can work on other parts of the proof. If they
wait for my explanation for the first error that they do not know how to correct,
they have to stop their work about  20 minutes. That means that I just cannot teach
without errors recovery.


> In the realm of programming languages like C, C++ or Java, syntactic
> errors after the first one are typically total bogus.  In C++, where
> identification is complicated, paying attention to any other but the
> first identification error is just waste of time.

So, there is no errors recovery in these languages. So what?

Andrzej