There have been a bunch of complaints about the formal semantics: it's no longer up to date, it has been incomplete since the beginning, it cannot be mechanized with a proof assistant, it doesn't help either users or implementers very much, and so on. See in particular #453.
This proposal is to remove it from the report altogether, and to urge the Steering Committee to create a new WG to produce one, likely in a "rolling" style with increasingly comprehensive releases, on its own schedule. Some members of the current WG have expressed interest in serving on such a group, and others have expressed their complete lack of interest, so a new WG seems the best choice if this is done.
WG1 voted to retain the formal semantics.