Real-world programming languages have subtle behaviours. In particular, their semantics is often associated with various corner cases. Programmers are sometimes unaware of all these corner cases, which can yield to serious bugs. This is an opportunity for our community as Coq provides a way to certify the behaviour of a program. But if the certified program is not written in Coq, such a certification relies on a formal semantics of its programming language. In the case of a real-world language, such a semantics can be as difficult to trust as the original program. Some previous work proposed ways to trust such large semantics. This work evaluates the feasibility of such a large-scale formalisation in the case of the R programming language—a trending programming language specialised in statistics. We introduce a formalisation of the core of R related to the reference R interpreter.