# 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:** 15\
**Page:** 2

<div class="post-metadata">

**Author:** ![robinm](https://sea2.discourse-cdn.com/flex002/user_avatar/internals.rust-lang.org/robinm/32/6255_2.png) [@robinm](https://internals.rust-lang.org/u/robinm)\
**Post date:** [January 20, 2021, 11:39pm UTC](https://internals.rust-lang.org/t/pre-rfc-extending-where-clauses-with-limited-formal-verification/13791/22 "2021-01-20T23:39:22Z")

</div>

> ..would conditions then become part of a function type? Functions/closures can be arguments to methods.. And so conditions can be in co- or contra-variant position.

In the proposition I made, the only action required by the compiler is to not repeat the assertion, when using the _exact same predicate_ and thus explicitly not part of the type system. The goal was to allow dead simple conforming implementations. This means that generating assertion at the top/bottom of the function is probably already enough, assuming that the optimizer is able to remove duplicates, across function calls. Otherwise all pre and post conditions can be generated in the caller, which make the de-duplication of assertion even easier. Of course a smart compiler could propagate those assertions in the type system, or any kind of AST decorations, use them for optimization, smartly decide between generating them at caller or callee side, … but it is not required to do so.

---

<div class="post-metadata">

**Author:** ![atagunov](https://sea2.discourse-cdn.com/flex002/user_avatar/internals.rust-lang.org/atagunov/32/5877_2.png) [@atagunov](https://internals.rust-lang.org/u/atagunov)\
**Post date:** [January 20, 2021, 11:48pm UTC](https://internals.rust-lang.org/t/pre-rfc-extending-where-clauses-with-limited-formal-verification/13791/23 "2021-01-20T23:48:39Z")

</div>

> [@robinm](#):
>
> Otherwise all pre and post conditions can be generated in the caller

I guess not in the case of a function passed as a parameter to another function? Since assertions are not part of the function type the compiler won't be able to insert them before invoking a function pointer..

---

<div class="post-metadata">

**Author:** ![robinm](https://sea2.discourse-cdn.com/flex002/user_avatar/internals.rust-lang.org/robinm/32/6255_2.png) [@robinm](https://internals.rust-lang.org/u/robinm)\
**Post date:** [January 21, 2021, 12:09am UTC](https://internals.rust-lang.org/t/pre-rfc-extending-where-clauses-with-limited-formal-verification/13791/24 "2021-01-21T00:09:46Z")

</div>

> What about function pointers?

The above model is too simplistic.

Post-condition can be inconditionaly generated at the end of the function.

For the pre-condition, instead of generating some assemby like this:

```rust
foo:
    // stack pointer and register set-up
    // rest of the code
    // tear done
    ret

```

Then this could be generated:

```rust
foo:
    // stack pointer and register set-up
    // assertion
    goto __1
foo_unchecked:
    // stack pointer and register set-up
__1:
    // rest of the code
    // tear done
    ret

```

And then callers that can prove the pre\_condition can replace call to `foo` by call to `foo_unchecked`. A call through a function pointer will always call the normal checked version.

---

<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)

---

<div class="post-metadata">

**Author:** ![H2CO3](https://sea2.discourse-cdn.com/flex002/user_avatar/internals.rust-lang.org/h2co3/32/2849_2.png) [@H2CO3](https://internals.rust-lang.org/u/H2CO3)\
**Post date:** [January 21, 2021, 6:28am UTC](https://internals.rust-lang.org/t/pre-rfc-extending-where-clauses-with-limited-formal-verification/13791/26 "2021-01-21T06:28:24Z")

</div>

> [@robinm](#):
>
> Let think about it again:

This whole thing looks like just some syntactic sugar for strategically placed `assert!()`s, that you somehow expect to be "removed" anyway. Unless we get full-fledged dependent typing, there's no way arbitrary expressions can be tied to types. At that point, doing this whole preconditions-postconditions dance really doesn't gain much of anything.

> [@robinm](#):
>
> They are just written in a form that can be easily checked by an external tool.

Alright, so the gain would be easier machine-discoverability. But I still don't get why that needs to be a core language feature? You can slap an attribute-like proc-macro on any function. Calling the proc-macro can transform the function body in an arbitrary way, so it might as well add assertions – it can even parse and modify the `where` clause however it pleases.

And then we have `syn` which can parse all Rust syntax including attributes, so it can be used by those external tools to gather the information from the attributes. Ideally, the proc-macro crate that performs the transform would actually expose its parsing API in order to provide a typed AST that 3rd-party tools can reuse.

> [@robinm](#):
>
> And `impl` of a trait can remove pre-condition and/or add post-condition (edited) to any method of the trait.

Whoa, whoa. Please let's not get into subtyping just yet. With great subtyping come great problems, such as variance and the like.

---

<div class="post-metadata">

**Author:** ![voidc](https://sea2.discourse-cdn.com/flex002/user_avatar/internals.rust-lang.org/voidc/32/8162_2.png) [@voidc](https://internals.rust-lang.org/u/voidc)\
**Post date:** [January 21, 2021, 11:28pm UTC](https://internals.rust-lang.org/t/pre-rfc-extending-where-clauses-with-limited-formal-verification/13791/27 "2021-01-21T23:28:07Z")

</div>

Interestingly, Rust once had something similar in the form of typestates, which were removed [back in 2012](https://github.com/rust-lang/rust/commit/41a21f053ced3df8fe9acc66cb30fb6005339b3e). The documentation explaining this feature is still very interesting to read though!

---

<div class="post-metadata">

**Author:** ![gbutler](https://sea2.discourse-cdn.com/flex002/user_avatar/internals.rust-lang.org/gbutler/32/3670_2.png) [@gbutler](https://internals.rust-lang.org/u/gbutler)\
**Post date:** [January 22, 2021, 1:35am UTC](https://internals.rust-lang.org/t/pre-rfc-extending-where-clauses-with-limited-formal-verification/13791/28 "2021-01-22T01:35:27Z")

</div>

Is there something explaining what led to the removal of "TypeStates" from Rust? Anyone care to quickly summarize the arguments and conclusions?

---

<div class="post-metadata">

**Author:** ![mbrubeck](https://sea2.discourse-cdn.com/flex002/user_avatar/internals.rust-lang.org/mbrubeck/32/174_2.png) [@mbrubeck](https://internals.rust-lang.org/u/mbrubeck)\
**Post date:** [January 22, 2021, 5:50am UTC](https://internals.rust-lang.org/t/pre-rfc-extending-where-clauses-with-limited-formal-verification/13791/29 "2021-01-22T05:50:38Z")

</div>

This Stack Overflow thread describes some of the reasoning: [rust - What is typestate? - Stack Overflow](https://stackoverflow.com/questions/3210025/what-is-typestate)

---

<div class="post-metadata">

**Author:** ![atagunov](https://sea2.discourse-cdn.com/flex002/user_avatar/internals.rust-lang.org/atagunov/32/5877_2.png) [@atagunov](https://internals.rust-lang.org/u/atagunov)\
**Post date:** [January 22, 2021, 5:59pm UTC](https://internals.rust-lang.org/t/pre-rfc-extending-where-clauses-with-limited-formal-verification/13791/30 "2021-01-22T17:59:51Z")

</div>

> [@H2CO3](#):
>
> > [@robinm](#):
> >
> > And `impl` of a trait can remove pre-condition and/or add post-condition (edited) to any method of the trait.
> 
> Whoa, whoa. Please let's not get into subtyping just yet. With great subtyping come great problems, such as variance and the like.

This is exactly the point that would be interesting to set straight. What @robinm suggested

- on the one hand expressly _is not_ a type system change
- yet this relation between a trait and its `impl` hugely resembles subtyping

Could somebody (selfish plea) help me understand, if this is a type system change or not? Is there really any subtyping relation between a trait and `struct`s on which it's `impl`? Would there be any more co- and contra- varience involved - more than already spelled out - if the feature was implemented?

---

<div class="post-metadata">

**Author:** ![sighoya](https://avatars.discourse-cdn.com/v4/letter/s/a87d85/32.png) [@sighoya](https://internals.rust-lang.org/u/sighoya)\
**Post date:** [February 12, 2021, 6:48pm UTC](https://internals.rust-lang.org/t/pre-rfc-extending-where-clauses-with-limited-formal-verification/13791/31 "2021-02-12T18:48:51Z")

</div>

> [@atagunov](#):
>
> Would there be any more co- and contra- varience involved - more than already spelled out

I think not presuming the exclusion of any lifetime semantics but it more kinda depends on propositional vs semantic subtyping.

> Could somebody (selfish plea) help me understand, if this is a type system change or not?

Where clauses acting as runtime assertions only wouldn't change the type system at least not by disregarding assertion errors as a possible Result of a function. But they change semantics of the program because they are able to abort it.

---

<div class="post-metadata">

**Author:** ![sighoya](https://avatars.discourse-cdn.com/v4/letter/s/a87d85/32.png) [@sighoya](https://internals.rust-lang.org/u/sighoya)\
**Post date:** [February 12, 2021, 6:57pm UTC](https://internals.rust-lang.org/t/pre-rfc-extending-where-clauses-with-limited-formal-verification/13791/32 "2021-02-12T18:57:00Z")

</div>

> [@robinm](#):
>
> Pre and post condition can be added to trait method (and thus should be copied into every `impl` of that trait). And `impl` of a trait can remove pre-condition and/or add post-condition (edited) to any method of the trait.

This was part of the problem regarding the contract proposal of C++, you could simply disable assertion checks, but what happens if the optimizer transforms code anyway even if the preconditions didn't hold?

Either we can't optimize, but we can disable checks, or we can optimize but are required to retain preconditions.

I think where clauses should be mandatory and not be disabled by unsafe tags, otherwise we could likewise state:

```Rust
unsafe i:i32="Hello World"

```

---

<div class="post-metadata">

**Author:** ![atagunov](https://sea2.discourse-cdn.com/flex002/user_avatar/internals.rust-lang.org/atagunov/32/5877_2.png) [@atagunov](https://internals.rust-lang.org/u/atagunov)\
**Post date:** [February 12, 2021, 7:42pm UTC](https://internals.rust-lang.org/t/pre-rfc-extending-where-clauses-with-limited-formal-verification/13791/33 "2021-02-12T19:42:23Z")

</div>

Hi there!

> [@sighoya](#):
>
> ... but it more kinda depends on propositional vs semantic subtyping

...doesn't this sound a bit cryptic?

---

<div class="post-metadata">

**Author:** ![sighoya](https://avatars.discourse-cdn.com/v4/letter/s/a87d85/32.png) [@sighoya](https://internals.rust-lang.org/u/sighoya)\
**Post date:** [February 12, 2021, 10:45pm UTC](https://internals.rust-lang.org/t/pre-rfc-extending-where-clauses-with-limited-formal-verification/13791/34 "2021-02-12T22:45:52Z")

</div>

> [@PabloMansanet](#):
>
> How would you feel if the SMT implementation was by design limited to the decidable subset of theories, or even a very simple subset of those? (e.g. just integer arithmetic)

It is possible, but:

- Even if your function is pure, it is also eligible in receiving non-deterministic values requiring to parametrize all unknowns, e.g. length after array concatenation is then m+n, again m+n+o...., branching makes it even worse: m+n+o | q+p.
- Inferring such parameters and let them bubble up implicitly causes additional compiler hits and becomes much harder to satisfy against preconditions as more unknowns come in that need to be tracked which may probably could be alleviated by subsuming them with one non-deterministic variable and two bound variables.
- Existing traits may aren't able to be equipped with these constraints as it might break implementations.
- Verifying the collection updating its length doesn't guarantee that the collection adds indeed the desired amount of elements. For this we need more powerful logic which may become undecidable.
- ARC may require implicit synchronization, bubbling up constraints prolongs the synchronization phase.
- Specialization requires to solve an (possible non-) linear integer problem.
- Semantics of control structures like for and while have also to be incorporated into the compiler's knowledge, e.g.

```Rust
for i =0 ... n, j=0 .. n-1 array.add(a) //=> array.length+=n*(n-1) 

```

or

```Rust
for i =1 ... (n+1) array.extend(anotherArray[0...i]) //=> n(n+1)/2 

```

---

<div class="post-metadata">

**Author:** ![sighoya](https://avatars.discourse-cdn.com/v4/letter/s/a87d85/32.png) [@sighoya](https://internals.rust-lang.org/u/sighoya)\
**Post date:** [February 12, 2021, 10:56pm UTC](https://internals.rust-lang.org/t/pre-rfc-extending-where-clauses-with-limited-formal-verification/13791/35 "2021-02-12T22:56:01Z")

</div>

> [@atagunov](#):
>
> ...doesn't this sound a bit cryptic?

Touché, I mean if we consider x\<=y simply as a membership of `(x,y)` to the relation `<=` (propositional logic, 0/1) or did we consider quantitative properties of `<=` like reflexivity and transitivity expressed over Higher order logic (HOL defining semantic).

The latter is more subtle as it allows simplifying for example `(x<=3) && (x<=4)` to `(x<=3)` but is generally undecidable and harder to solve.

---

<div class="post-metadata">

**Author:** ![system](https://sea2.discourse-cdn.com/flex002/user_avatar/internals.rust-lang.org/system/32/14092_2.png) [@system](https://internals.rust-lang.org/u/system)\
**Post date:** [May 13, 2021, 10:56pm UTC](https://internals.rust-lang.org/t/pre-rfc-extending-where-clauses-with-limited-formal-verification/13791/36 "2021-05-13T22:56:28Z")

</div>

Closed on May 13, 2021, 10:56pm UTC

This topic was automatically closed 90 days after the last reply. New replies are no longer allowed.

[Previous page](https://internals.rust-lang.org/t/pre-rfc-extending-where-clauses-with-limited-formal-verification/13791.md?page=1)