This going to be the easiest way forwards. There are just too many, inconsistent definitions of “pedantic” to have a self-consistent set of checks.
For example checks based on naming conventions are going to be dangerous when jumping between fields where those name conventions no longer hold.
In some sense the parser/compiler is the pedantic mode, pedantically allowing any program that defines a valid probabilistic program (for the Stan definition of probabilistic program defining a log joint density). Beyond that is heuristics that attempt to identify causes of not a user specifying an invalid program but rather a different program than what they wanted. Categorizing these heuristics will help to avoid getting bogged down in differing opinions while also communicating to the user what is being assumed in the generation of the warning.
One mode could be based on graphical model heuristics, checking that every parameter is assigned a single prior density (i.e. the variable is on the left hand side of one and only one density increment). Within this mode we could also check those densities against the constraints of the parameters and flag inconsistencies.
One mode could be based on programming heuristics such as not using an undefined variable or, perhaps more important, not explicitly assigning values to local variables. This is a super common mistake when people type “variable[N] = 1” instead of “variable[n] = 1” in a loop. Another check would be when vectorization is used within a loop to try and catch accidentally redundant priors.
One mode could subsume the Jacobian warning that we already have.
Perhaps one mode based on looking for inefficient patterns? Such as vectorization opportunities, unneeded matrix inversions, etc.
Beyond that we get into murkier territory, including modeling recommendations (prior choices) and naming conventions.