why is carbon baing intentionally opressed/constrained ,why not make it free

[gintominto5329]

rust has merely one bold feature ,absent in carbon ;which is formal-verification ,that too ,to quite an extreme ,extent.

why can this feature ,to an extent ,be bought to carbon ,but fully optional ,with function/class boundaries ,with a qualifier(like "safer") ,

this can even destroy rust ,because of its many problem ,and no longer being the only ,formally-verified code producing lang.

thanks

[chandlerc]

I don't fully understand this, but I think the phrasing in this discussion isn't the approach we want in Carbon forums.

Nothing is oppressing or intentionally constraining Carbon. We're pursuing a specific set of goals that are different from Rust's goals. We also are starting from a very different point than Rust.

There are many features of Rust that are different from Carbon, not just its features around memory safety (which you're calling "formal-verification" I think? see below). We do have interest in adding a safe dialect to Carbon, and plan to work on this in the [future], but it isn't our current focus.

Regarding formal-verification -- that term is typically used in programming languages differently. Formal verification of software typically means proving the software completely correct. Type systems, including Rust's type systems, provide a way to prove some aspects of software's behavior, but typically not all of it. There are more advanced formal methods that build on top of type systems to formally verify the entire behavior of software though. But that's not really a feature of Rust, it's somewhat independent.

Anyways, and maybe more importantly, our goal is not to destroy Rust. As we state in our documentation -- if you can use Rust, you should. It's a great language. Discussions of how to destroy other languages aren't really on-topic for Carbon forums so I'm going to close this therad before it goes further off topic.