rust
/
reference
mirror of https://github.com/rust-lang/reference
1
0
Fork 0
Code Issues Releases Wiki Activity

Improve wording of unsafe proof obligations. 

Co-authored-by: Ralf Jung <post@ralfj.de>
This commit is contained in:
Greg Schmit 2023-07-18 22:27:30 -05:00 committed by GitHub
parent 3c3c084d03
commit 451a8e4542
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
1 changed files with 1 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
src/unsafe-keyword.md
View File

@ -29,7 +29,7 @@ By putting operations into an unsafe block, the programmer states that they have
Unsafe blocks are the logical dual to unsafe functions:
where unsafe functions define a proof obligation that callers must uphold, unsafe blocks state that all relevant proof obligations of functions or operations called inside the block have been discharged.
There are many ways to discharge proof obligations;
for example, there could be run-time checks or data structure invariants that guarantee that certain properties are definitely true, or the unsafe block could be inside an `unsafe fn`, in which case the block can use the proof obligations of that function to discharge the proof obligations of any unsafe functions called inside the block.
for example, there could be run-time checks or data structure invariants that guarantee that certain properties are definitely true, or the unsafe block could be inside an `unsafe fn`, in which case the block can use the proof obligations of that function to discharge the proof obligations arising inside the block.
Unsafe blocks are used to wrap foreign libraries, make direct use of hardware or implement features not directly present in the language.
For example, Rust provides the language features necessary to implement memory-safe concurrency in the language but the implementation of threads and message passing in the standard library uses unsafe blocks.