A programming language formalization gives a single source of truth about the language behavior. Unless mechanized, a formalization can be erroneous and logically unsound. Mechanizing a formalization can guarantee that the semantics of the language is sound, and that the formalization is free of bugs. For a complex language, however, mechanization is laborious, as is maintaining an existing mechanization as the language evolves. Mechanizations are usually monolithic, such that each new feature requires manually rewriting existing code. At its core, this is due to the manifestation of the expression problem for inductive types. Several solutions have been proposed to improve proof reuse in mechanizations, and some have found use in practice. Our work targets JavaScript semantics with approach developed in Coq à la Carte. We aim to show that it is possible to reason about modern heavily used languages in a modular fashion, keeping mechanization open to extension with new features.