Skip to content

Commit

Permalink
Remove 'unchecked' from docs
Browse files Browse the repository at this point in the history
  • Loading branch information
brson committed Sep 18, 2012
1 parent 76c8b83 commit 5e9d38e
Showing 1 changed file with 17 additions and 16 deletions.
33 changes: 17 additions & 16 deletions doc/rust.md
Original file line number Diff line number Diff line change
Expand Up @@ -222,7 +222,7 @@ pure
return
struct
true trait type
unchecked unsafe
unsafe
while
~~~~~~~~

Expand Down Expand Up @@ -1035,23 +1035,24 @@ pure fn nonempty_list<T>(ls: List<T>) -> bool { pure_length(ls) > 0u }

*TODO:* should actually define referential transparency.

The effect checking rules previously enumerated are a restricted set of
typechecking rules meant to approximate the universe of observably
referentially transparent Rust procedures conservatively. Sometimes, these
rules are *too* restrictive. Rust allows programmers to violate these rules by
writing pure functions that the compiler cannot prove to be referentially
transparent, using an escape-hatch feature called "unchecked blocks". When
writing code that uses unchecked blocks, programmers should always be aware
that they have an obligation to show that the code *behaves* referentially
transparently at all times, even if the compiler cannot *prove* automatically
that the code is referentially transparent. In the presence of unchecked
blocks, the compiler provides no static guarantee that the code will behave as
expected at runtime. Rather, the programmer has an independent obligation to
verify the semantics of the pure functions they write.
The effect checking rules previously enumerated are a restricted set
of typechecking rules meant to approximate the universe of observably
referentially transparent Rust procedures conservatively. Sometimes,
these rules are *too* restrictive. Rust allows programmers to violate
these rules by writing pure functions that the compiler cannot prove
to be referentially transparent, using "unsafe blocks". When writing
code that uses unsafe blocks, programmers should always be aware that
they have an obligation to show that the code *behaves* referentially
transparently at all times, even if the compiler cannot *prove*
automatically that the code is referentially transparent. In the
presence of unsafe blocks, the compiler provides no static guarantee
that the code will behave as expected at runtime. Rather, the
programmer has an independent obligation to verify the semantics of
the pure functions they write.

*TODO:* last two sentences are vague.

An example of a pure function that uses an unchecked block:
An example of a pure function that uses an unsafe block:

~~~~
# use std::list::*;
Expand All @@ -1065,7 +1066,7 @@ fn pure_foldl<T, U: Copy>(ls: List<T>, u: U, f: fn(&&T, &&U) -> U) -> U {
pure fn pure_length<T>(ls: List<T>) -> uint {
fn count<T>(_t: T, &&u: uint) -> uint { u + 1u }
unchecked {
unsafe {
pure_foldl(ls, 0u, count)
}
}
Expand Down

0 comments on commit 5e9d38e

Please sign in to comment.