I'm interested in language design and in general I can reason easily about widely known features (e.g. inheritance, polymorphism, delegates, lambdas, captures, garbage collection, exceptions, generics, variance, reflection, and so on), their interactions in a particular language, the ways they can possibly be implemented, their limitations, etc.
In the last few months, I started reading about Rust, which has an ownership system that ensures memory safety and deterministic resource management by forcing object lifetimes to be statically verifiable. From the perspective of a plain user of the language, I could pick up the system almost immediately.
From the perspective of a language designer, however, it took me a while to realize why things in Rust are exactly the way they are. I couldn't immediately understand the reasoning behind some restrictions of the ownership system, until I forced myself to come up with cases that would violate the integrity of a system if it didn't have those aspects.
My main question has nothing to do with Rust and its ownership specifically -- but feel free to use it as an example in your comments/answers, if you need to.
When language designers design a new feature, what methodology or process do they use to decide that the feature works properly?
By "new" I mean that it's not something that has already been tested in existing languages (and thus the bulk of the work has been done by other designers). By "works properly" I mean that the feature solves the intended problem correctly, and it's reasonably bulletproof. By "reasonably bulletproof" I mean that no code can be written in the language or a particular subset of the language (e.g. a subset without "unsafe" code) that would violate the integrity of the feature.
Is it a trial and error process, in the sense that you come up with a simple form of the feature, then try to find ways to violate it, then patch it if you successfully violate it, then repeat? And then, when you can't think of any other possible violations, you hope there's nothing left and call it a day?
Or is there a formal way to actually prove (in the mathematical sense of the word) that your feature works and then use that proof to confidently get the feature right (or mostly right) from the start?
(I should mention that I have an engineering background, not computer science. So if I'm missing something that would be obvious to CS people, please feel free to point it out.)