I know I'm late to the party, but I still wanted to answer this. Disclosure: I am one of the Managing Directors at Ferrous Systems
I believe you're falling victim ot a common misconception about what the FLS is and what it aims to be. It is - at least as of now - a description of the language that is good enough to certify the compiler. It was never intended to be a spec that describes Rust in completeness - for example, the FLS is absolutely insufficient to implement a Rust compiler. As such, we have no aspirations to completeness in any shape or form. While we get a lot of feedback about pieces that people consider falling short of their expectations, it is expected that there are gaps that Ferrous Systems will never try to fill. The FLS in its current shape is good enough for us.
Now that the Rust project adopted the FLS as the initial nucleus of a spec, I hope that others can contribute and fill the gaps that they need filled.
From experience with these kinds of specs, one might be better off clearly stating things that are left to the compiler implementation (and thus should have no impact -?-on the verifiability of the spec).
I believe you're falling victim ot a common misconception about what the FLS is and what it aims to be. It is - at least as of now - a description of the language that is good enough to certify the compiler. It was never intended to be a spec that describes Rust in completeness - for example, the FLS is absolutely insufficient to implement a Rust compiler. As such, we have no aspirations to completeness in any shape or form. While we get a lot of feedback about pieces that people consider falling short of their expectations, it is expected that there are gaps that Ferrous Systems will never try to fill. The FLS in its current shape is good enough for us.
Now that the Rust project adopted the FLS as the initial nucleus of a spec, I hope that others can contribute and fill the gaps that they need filled.