Any complex project tends to have both explicitly stated and implicitly unstated target goals. For instance, a Lean formalization project may have as its explicit goal the task of obtaining a formal proof of some mathematical claim X; but there are often unstated goals, such as also formalizing key subclaims and definitions X_1, X_2, ... to X in a fashion that would be suitable for upstreaming to the Mathlib library; learning how to use various collaboration tools and distribute tasks; organically discovering insights to the finer structure of the proof of X that might not be emphasized in previous informal proofs; giving real-world training and experience to novice formalizers; and more generally building a community of humans expert in the art of formalization.

In the past, it has generally not been necessary to state these implicit goals because of a strong empirical correlation between the achievement of these goals and the achievement of the explicit goals. In the example of the formalization project, pretty much any human-centric effort to accomplish the explicit goal will end up naturally also achieving most of the implicit goals stated above. So the explicit goal effectively becomes a viable proxy for the broader range of actual goals. (1/2)

If anyone tells you that a string (like a command-line argument) contains a list of smaller strings with a specific separator character in between them, immediately ask "In that case, what happens if the separator character needs to appear in one of the list items?" Instant knee-jerk reflex.

There's more than one good answer. Like "you can escape the separator with this other character" (in which case you know what question #2 is). Or "here is a specific reason why it _can't possibly_ be necessary to put the separator in a list item" (maybe list items are something like numbers or C identifiers which already have a restricted character set).

But if they just say it doesn't seem _likely_, or worse still, demand you justify why you need to, run a mile from whatever software is under discussion.

@thephd I come to you with a cursed finding from a colleague and I: in N3220, and still in N3550, section 6.4.4.2 "Integer constants" is using U+2019 RIGHT SINGLE QUOTATION MARK everywhere, and never specifies otherwise, so it is _technically_ the standard digit separator in C and not U+0027 APOSTROPHE

https://github.com/cigix/cstdtohtml/issues/18

how far off do we think this is from being the default shell startup on every platform

https://thepit.social/@peter/114601765045842916