I endorse this, and IME find there are major benefits to “relaxing” even moreso through reductions or decompositions into well-known models rather than defining your own.
A lot of problems in practice are just too complex, too theoretically difficult, or some combination of not-theoretically-interesting-enough for an academic or specialized worker to be attracted/assigned/exposed to it, or just too difficult/expensive/time consuming/unimportant to be worth directly formally modeling. Or, they’re big problem spaces and you want to start where you get the most bang-for-your-buck. A (partial) reduction lets you still realize practical benefits for problems that may not perfectly or entirely be amenable to simple/small models, or which themselves may be “jagged”/gnarly problem domains due to real-world constraints like backwards compatibility.
Reduction to a formal target arise naturally from defining type conversions (likely to a codomain that is either actually a strict superset of the real reduction image, ie overly generalized/non-surjective, or bijective for some partial subset/step). Mathematically or computationally, it may be less than ideal to use an overly broad/flexible/general abstraction to model something more structured. But practically, it lets you use actual software written for the target reduction and apply any results/properties of the more familiar or better studied model.
The less-than-ideal reduction may be easily verifiable/simple and so obviously safe that, in-context, it’s clearly worth choosing the technically-suboptimal/less-elegant/partial approach to free ride off existing formal verification, without needing to wade deep into theoretical territory, than to chase perfection.
For example, if you can model a data format as a Context Free Grammar, or a subset of all context free grammars, a developer could spell out that grammar or grammars and then use existing metaparsing tools to safely process input data rather than write their own parser. And they wouldn't even need the format to be a complete CFG to leverage CFG tooling! Suppose portions are context-sensitive - for example, decoding the payload requires applying some length-prefix extracted from the header - just encode and parse the header format as a CFG with an opaque payload blob suffix with a length equal to eg the max payload/packet/fragment size. Perhaps some part of the header also specifies the payload’s structure in addition to the length: you could have one CFG for reading the header, a simple wrapping CFG for a fixed-length frame containing a header followed by junk (FRAME_HEADER_CFG :=, a CFG for each payload format, and one wrapping/router function that handles the very simple non-cfg step of using the first-pass parsing output to determine the length/format of the second pass.
FRAME_HEADER_CFG := HEADER_CFG {BYTE}
...
Parse(byte[] in) {
AST frame = ParseCFG(FRAME_HEADER_CFG, in[:FRAME_SIZE]);
Header h, byte[] p = frame[0], frame[1];
assert(len(p) >= h.payload_size);
return ParseCFG(PAYLOAD_CFGS[h.payload_type], in[FRAME_SIZE-len(p):h.payload_size]);
}
Then even though your data format is not technically a CFG, the vast majority of your parsing occurs within a CFG, with only a small part that does (in pseudocode). And you did not have to do or run any formal verifications, or use special model checkers, only encode the CFG-compatible subsets of your data format into something like EBNF, then use a compatible formally-verified metaparser, and take a leap of faith that the small amount of non-formally-verified/not-nice-to-model code is safe. That's much more realistic for a developer to do than to implement a formal-verification of a non-cfg format de novo.