Add second section of the tutorial#481
Merged
Merged
Conversation
Comment on lines
+136
to
+150
| ## Future work | ||
|
|
||
| RMC notably does not check the following: | ||
|
|
||
| 1. Concurrency bugs, deadlocks, or data races. | ||
| It's possible RMC may be extended in the future to find such issues. | ||
|
|
||
| 2. Rust type invariants. | ||
| For example, it's undefined behavior in Rust to produce a value of type `bool` that isn't `0` or `1`. | ||
| RMC will not spot this error (in presumably unsafe code), yet. | ||
|
|
||
| 3. Fully generic functions. | ||
| To write a proof harness and call functions, they must be fully "monomorphized." | ||
| This means we can't currently check a generic function (`foo<T>`) generically. | ||
| Proof harnesses have to be written specializing type parameters (`T`) to concrete types (e.g. `u32`), and check those instead. |
Contributor
There was a problem hiding this comment.
I'd prefer to link to the dashboard so this information doesn't become stale
Contributor
Author
There was a problem hiding this comment.
I tried to stick to bigger ideas here than what the dashboard really shows. Set people's expectations appropriately.
Contributor
There was a problem hiding this comment.
Ok, in that case, could we make the statement "does not currently check"?
zhassan-aws
reviewed
Sep 14, 2021
| - [RMC on a crate]() | ||
| - [Debugging failures]() | ||
|
|
||
| - [Debugging non-termination]() |
Contributor
There was a problem hiding this comment.
Is this section coming in the next batch? If so, should we take it out from this PR?
Contributor
Author
There was a problem hiding this comment.
mdbook supports "outlining" like this as a specifically added feature. Seems nice to use, and it makes the planned structure visible.
zhassan-aws
approved these changes
Sep 14, 2021
zhassan-aws
left a comment
zhassan-aws
left a comment
Contributor
There was a problem hiding this comment.
Great examples, @tedinski!
tedinski
added a commit
to tedinski/rmc
that referenced
this pull request
Apr 26, 2022
* initial draft of 2nd tutorial section * add exercise solutions, fix minor issues
tedinski
added a commit
that referenced
this pull request
Apr 27, 2022
* initial draft of 2nd tutorial section * add exercise solutions, fix minor issues
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
3 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Description of changes:
This adds section 2/3 of the currently planned RMC tutorial.
Resolved issues:
Towards #254
Call-outs:
Testing:
How is this change tested? Each example in the cargo package fails RMC.
Is this a refactor change? No
Checklist
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.