Skip to content

Commit

Permalink
fix typos
Browse files Browse the repository at this point in the history
Merge remote-tracking branch 'lqd/typoman-is-back'
  • Loading branch information
nikomatsakis committed May 31, 2024
2 parents c2b6637 + 066eef1 commit 08efe87
Show file tree
Hide file tree
Showing 3 changed files with 3 additions and 3 deletions.
2 changes: 1 addition & 1 deletion src/2024h2/Contracts-and-invariants.md
Original file line number Diff line number Diff line change
Expand Up @@ -14,7 +14,7 @@ Second, we want to extend the Rust crate format such that the contracts for a cr
Third, we want to extend project-supported Rust compiler and interpreter tools, such as `rustc` and `miri`, to compile the code in a mode that dynamically checks the associated contracts (note that such dynamic checking might be forced to be incomplete for some contracts).
Examples of contracts we envision include: pre- and post-conditions on Rust methods; representation invariants for abstract data types; and loop invariants on `for` and `while` loops.

Our motivation for this is that contracts are key for reasoning about software correctness. Formal verification tools such as [Creusot][], [Kani][], and [Verus][] have demonstrated that it is possible to write Rust code that is coupled with automated verification mechanisms. But furthermore, we assert that contracts can provide value even if we restrict our attention to dynamic checking: By having a dedicated construct for writing method specifications and invariants formally, we will give our tools new avenues for testing our programs in an automated fashion, similar to the benefits provdied by fuzzing.
Our motivation for this is that contracts are key for reasoning about software correctness. Formal verification tools such as [Creusot][], [Kani][], and [Verus][] have demonstrated that it is possible to write Rust code that is coupled with automated verification mechanisms. But furthermore, we assert that contracts can provide value even if we restrict our attention to dynamic checking: By having a dedicated construct for writing method specifications and invariants formally, we will give our tools new avenues for testing our programs in an automated fashion, similar to the benefits provided by fuzzing.

[Creusot]: https://github.com/creusot-rs/creusot?tab=readme-ov-file#about
[Kani]: https://model-checking.github.io/kani/
Expand Down
2 changes: 1 addition & 1 deletion src/2024h2/Project-goal-slate.md
Original file line number Diff line number Diff line change
Expand Up @@ -134,7 +134,7 @@ It is not yet clear how much work it will be to drive this process. If needed, t

### Is there a template for project goals?

This RFC does not specify details, so the following should not be considered normative. However, you can see a preview of what the project goal process would look like at the [nikomatsakis/rust-project-goals](https://github.com/nikomatsakis/rust-project-goals) repository; it contains a [goal template](https://nikomatsakis.github.io/rust-project-goals/2024h2/0000-TEMPLATE.html). This RFC is in fact a "repackaged" vesion of [2024's proposed Project Goal #1](https://nikomatsakis.github.io/rust-project-goals/2024h2/0001-Project-goal-slate.html).
This RFC does not specify details, so the following should not be considered normative. However, you can see a preview of what the project goal process would look like at the [nikomatsakis/rust-project-goals](https://github.com/nikomatsakis/rust-project-goals) repository; it contains a [goal template](https://nikomatsakis.github.io/rust-project-goals/2024h2/0000-TEMPLATE.html). This RFC is in fact a "repackaged" version of [2024's proposed Project Goal #1](https://nikomatsakis.github.io/rust-project-goals/2024h2/0001-Project-goal-slate.html).

### Why is the goal completion date targeting end of year?

Expand Down
2 changes: 1 addition & 1 deletion src/2024h2/slate.md
Original file line number Diff line number Diff line change
Expand Up @@ -40,7 +40,7 @@ Note that committing to a goal means that the teams support the next few steps a
[Fallible allocation]: ./Fallible-allocation.md
[Intrusive linked lists]: ./Intrusive-linked-lists.md

[own]: https://img.shields.io/badge/Owned%20Needed-blue
[own]: https://img.shields.io/badge/Owner%20Needed-blue

[acc]: https://img.shields.io/badge/Accepted-green
[prov]: https://img.shields.io/badge/Provisional-yellow
Expand Down

0 comments on commit 08efe87

Please sign in to comment.