Re: GNUism in groff tests, was: pic anomalies

[Tadziu Hoffmann]

>  A debugging build I made in December is about 20k lines
>  before the preprocessor runs and about 30k afterwards.
>  The formal verification code, written in Isabelle/HOL[2],
>  is about an order of magnitude greater than that.

Just out of curiosity (since I'm unfamiliar with the concepts),
what is the code complexity like?  If the verification code is
larger, is it also more complex?  If yes, can the verification
code somehow be checked against possible errors as well?