# Pre-RFC: Extending where clauses with limited formal verification

**URL:** https://internals.rust-lang.org/t/pre-rfc-extending-where-clauses-with-limited-formal-verification/13791
**Category:** language design
**Created:** [January 9, 2021, 2:36pm UTC](https://internals.rust-lang.org/t/pre-rfc-extending-where-clauses-with-limited-formal-verification/13791 "2021-01-09T14:36:52Z")
**Posts on this page:** 1
**Showing post:** 25

<div class="post-metadata">

### Author: ![scottmcm](https://sea2.discourse-cdn.com/flex002/user_avatar/internals.rust-lang.org/scottmcm/32/2355_2.png) [@scottmcm](https://internals.rust-lang.org/u/scottmcm)
#### Post date: [January 21, 2021, 2:00am UTC](https://internals.rust-lang.org/t/pre-rfc-extending-where-clauses-with-limited-formal-verification/13791/25 "2021-01-21T02:00:33Z")

</div>

> [@robinm](#):
>
> And then callers that can prove the pre\_condition can replace call to `foo` by call to `foo_unchecked` .

You can actually use inlining as a way to do that. See the construction I describe in [Idea: make assert!() a keyword - REJECTED - #8 by scottmcm](https://internals.rust-lang.org/t/idea-make-assert-a-keyword-rejected/13066/8)

---

_[View the full topic](https://internals.rust-lang.org/t/pre-rfc-extending-where-clauses-with-limited-formal-verification/13791)._