One of the early certifying compilers was implemented in it, too. Done by the same company that verified and certified MULTOS OS (plus Mondex prototype). They did a Z spec of a small, imperative language and idealized, assembly language. Refined the specs into Prolog as a cheat: execute the specs almost directly after the refinement instead of rough conversion to lower-level program. Reuses Prolog implementation & verification work. Same method was used for a real compiler by defense contractor for safety-critical work. One of neatest uses of Prolog compilation I’ve seen outside AI stuff.
The reddit discussion here has more context.
A compiler implemented in prolog, awesome.
One of the early certifying compilers was implemented in it, too. Done by the same company that verified and certified MULTOS OS (plus Mondex prototype). They did a Z spec of a small, imperative language and idealized, assembly language. Refined the specs into Prolog as a cheat: execute the specs almost directly after the refinement instead of rough conversion to lower-level program. Reuses Prolog implementation & verification work. Same method was used for a real compiler by defense contractor for safety-critical work. One of neatest uses of Prolog compilation I’ve seen outside AI stuff.
http://www-users.cs.york.ac.uk/susan/bib/ss/hic/