[Omake] Could metaprl be used to create omake?

[Larry Evans]

Although currently, omake is used to create metaprl:

  http://metaprl.org/install.html

I'm wondering if metaprl could be used to formally specify
what omake does and then generate the code to satisfy
that specification.  From a cursory reading of:

  http://metaprl.org/user-guide/default.html

which contains:

  their proofs in the implementation are /programs/.

I'm assuming that in that a side effect of the proof is
a program (i.e. omake) which satisfies the specification.
Is that assumption correct?  If so, then why wouldn't
it be good to use metaprl to create omake?

TIA.