For historical reasons we've allowed inconsistent browser-default styles to apply to textarea#wpTextbox1 (and until recently we allowed the browser to set the font family: T170223)
This leads to inconsistency across browsers, which can lead to a jarring UX when changing browser, and also problems implementing new edit areas with a consistent feel (e.g. Flow, VE source mode), or extensions that require font-size matching (e.g. CodeMirror syntax highlighting, see T180678)
The issue is further complicated by the fact we use font-family:monospace (instead of the "monospace, monospace" hack: T176636) which applies extra font size rules in some browsers (Firefox) and some versions.
The current font sizes we get are (all in px):
| Browser | OS | Monospace | Serif/Sans-serf | Notes
| ---- | ---- | ---- | ---- | ---- |
| Chrome | Win/Ubuntu | 13.3333 | 13.3333 | (Likely more precision, but reporting tool rounds to 4dp)
| IE/Edge | Win (All) |13.33 | 13.33 | (as above)
| Firefox | OSX/Win | 13 | 16
| Firefox | Ubuntu | 12 | 16
| Safari | OSX (All) |11 | 11
| Chrome | OSX | 11 | 11
It would seem sensible to standardise on 13.3333 to affect the fewest number of users. Chrome+IE/Edge users (76%) will be unaffected except for OSX (~4%). Firefox users (15%) will get a barely noticeable change. The only users significantly affected will be OSX users (12%) who will notice a significant increase (from the currently very small, and arguably not-very-accessible 11px).
Edit: Also FF users who have changed their edit font to serif/sans-serif will get a significant change, but very few people use that preference at all (https://phabricator.wikimedia.org/T170223#3539911)
Edit2: We are going with 13px. It should be basically indistinguishable from 13.3333px, and avoids rounding errors further down the chain.