Proposal: remove decimal syntax with no leading zero from language (.1234)

[ahelwer]

Another issue along with #18 intended as a good warmup for the Specification Language Committee (SLC) process. Currently, the TLA+ language standard allows users to write decimal literals without a leading zero, like ".1234"; see: https://github.com/tlaplus/tlaplus-standard/blob/652a8eb5d5838b9712be3502cb36dbae826d5689/grammar/TLAPlus2Grammar.tla#L38

However, neither SANY nor TLAPM actually support this; see:

• SANY differs from TLA+ language spec for parsing number values with decimals tlaplus#596
• TLAPM fails to parse decimal numbers of form .12345 without leading zero tlapm#173

Currently, only the tree-sitter grammar supports this functionality. Given that "Section 16.1.11: Numbers" on page 308 of Specifying Systems makes no mention of this curious syntax (every other programming language I can think of requires a leading zero for decimal literals), it is entirely likely that this is a typo in the formal TLA+ grammar and the regex was meant to be Numeral+ & {"."} & Numeral+ instead of Numeral* & {"."} & Numeral+.

However, we needn't waste time speculating - we can decide the truth for ourselves! This RFC proposes to define decimal literals as requiring a leading zero. The work required to ratify this RFC is fairly minor:

1. Update the formal TLA+ grammar document in the tlaplus-standard repo
2. Update the tree-sitter grammar to disallow this syntax
3. Add a regression test to the old_syntax.txt syntax corpus document to ensure all conformant TLA+ parsers reject decimal literals lacking a leading zero
4. Write a short document outlining this change to be placed somewhere for the record, probably a directory in the tlaplus-standard repo

[IamfromSpace]

I'd agree that this seems like the right way to go. If it was part of the spec and never actually supported and no ever seemed to mind, we might as well remove it from the spec.