pi = 3.14159
e = 2.71828
と
e = 3.14159
pi = 2.71828
で「後者に違和感を持つのは間違い」という奴の
形式仕様は読みたくないな

形式仕様からプログラムコードを自動生成してメンテナンスフリーというならともかく
それがソフトウェアなり何なりの「仕様」を定めている以上
非形式的な意味は持たせてもいいし
それによって非形式的仕様になる訳じゃない

非形式的な意味は形式的検証の結果に影響を与えないのだから