Re: [mizar] Why doesn't this behave like I expect?

[Josef Urban <urban@ktilinux.ms.mff.cuni.cz>]

Hi Freek,

>   It tries to access memory it shouldn't try to. Strange... I
>   thought pascal had no pointers and thus couldn't make that
>   kind of errors. 

It has pointers, it is very close to C++ today - fairly low-level language 
with the guarantee that 90% of programmer's time is spent on memory bugs 
:-( (but in C++ they at least have good garbage collectors).

> Someone should be using OCaml :)

Sure, the code size would probably drop very much - just now I was looking 
at some code essentially implementing shared terms and their garbage 
collecting (it's called "inference constants" in Mizar). All these things 
are for free in sane languages, and usually implemented better than anyone 
doing his own small-scale shared-and-garbage-collected data is willing to.
So with a compiled language like OCaml, the speed might even increase 
(though it does not matter too much).
Producing free Mizar implementation in OCaml would be a great service to 
the mankind :-).

Josef