I think the gap is real and for it to be resolved, the spec language needs to be elevated to a source of truth and possibly do some degree of codegen, which is currently not well realized with Lean

The analogy I'd make is to the idea of "type driven development" that buf/protoc represent, where one defines their types and schema in proto and then types for specific languages are generated from that

The limitations there however is that proto is not a programming language and inflexible/inexpressive whereas Lean is one of the most expressive languages to date