Should we formalize the OT Spec?

Belleve Invis

As OTVar being added, OpenType finally become a programming language somehow...
So should we formalize it, by defining the semantics of a font into a formalized language (like, Coq or Idris), and define the corresponded functions into it?

Here is an example of formalized algorithm of calculating a "value + delta" quantity: https://gist.github.com/be5invis/cf7a3a0c8925cace3749986cf64f15fc

Dave Crossland

Do you mean like https://github.com/Pomax/A-binary-parser-generator/blob/master/OpenType.spec ?

Belleve Invis

Dave Crossland said:

Do you mean like https://github.com/Pomax/A-binary-parser-generator/blob/master/OpenType.spec ?

No, i mean formalize the semantics instead of binary representation of fonts. For example in the VQ I linked above, it is represented in many forms in different tables, but has the same meaning.