厳密な仕様があるのは理想だけど、規格化された言語ですら数学的に厳密な仕様なんて存在しないしな
最終的にはCoqのソースコードで示される、とかはあるかもしれないが