On 07/11/2023 10:09, Makarius wrote:
I first heard of "Unicode" approx. 1990. Everybody was talking about
"wide charaters" (16bit) and made moves to support them (e.g. major
Unix vendors and MicroSoft). That was the time of now obsolete UCS16:
"16bit should be sufficient for everyone, i.e. every imaginable
character on the planet".
We began working (at ICL) with Cambridge HOL in 1986, using a modified
version for an important secure hardware verification 88-9 before
starting the project which first developed ProofPower in 90-93.
The emphasis was on verification of systems specified in Z, and so at
first we had done small things to make HOL look more like Z, and one of
those was simply to use the extended character set.
At that time we were on Sun workstations, and Linux didn't exist.
Sun had a font editor, so I just added extra characters in the empty
spaces in the existing character sets and edited the font myself; things
were way simpler in those days.
There are of course things we would have used if they had been on our
radar. UTF would have been a good idea, and it would have been better
perhaps to have started out with an open source project, but we were
scuppered by the commercialisation by Cambridge University of the Poly
ML system which had been chosen as the best base for ProofPower (before
that happened).
Roger
_______________________________________________
Proofpower mailing list
[email protected]
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
