Function require_implementations 

pub fn require_implementations(
    project: &Project,
    diags: &mut Diagnostics,
) -> bool

Refuse a project that cannot run because one of its modules has no implementation.

Separate from check_project because “this typechecks against the contracts it was given” and “this can be executed” are two questions, and §3.6’s separate compilation is the first one being useful on its own: beck check and beck iface work against a .becki with no .beck beside it, and refusing that would delete the feature.

Executing is the other question. A module that contributed no bodies is simply absent from the link, so every call into it dangles and the failure arrives from the linker as no such definition — an absence, with nothing naming the module or saying why. B0604 already says the right thing and was reachable only when such a module was the root.