From 03baf55633ee0b77fa54474398bcedbeb27f9e46 Mon Sep 17 00:00:00 2001 From: Jorge Aparicio Date: Tue, 20 Nov 2018 00:24:24 +0100 Subject: [PATCH] static-guarantees: add intro text --- src/static-guarantees/index.md | 22 +++++++++++++++++++++- 1 file changed, 21 insertions(+), 1 deletion(-) diff --git a/src/static-guarantees/index.md b/src/static-guarantees/index.md index bd138f8..7e255c4 100644 --- a/src/static-guarantees/index.md +++ b/src/static-guarantees/index.md @@ -1,3 +1,23 @@ # Static Guarantees -> ❌: This section has not yet been written. Please refer to [rust-embedded/book#5](https://github.com/rust-embedded/book/issues/5) for discussion of this section. +It's Rust's type system what prevents data races at compile time (see [`Send`] +and [`Sync`] traits). The type system can also be used to check other properties +at compile time; reducing the need for runtime checks in some cases. + +[`Send`]: https://doc.rust-lang.org/core/marker/trait.Send.html +[`Sync`]: https://doc.rust-lang.org/core/marker/trait.Sync.html + +When applied to embedded programs these *static checks* can be used, for +example, to enforce that configuration of I/O interfaces is done properly. For +instance, one can design an API where is only possible to initialize a serial +interface by first configuring the pins that will be used by the interface. + +One can also statically check that operations, like setting a pin low, can only +be performed on correctly configured peripherals. For example, trying to change +the output state of a pin configured in floating input mode would raise a +compile error. + +And, as seen in the previous chapter, the concept of ownership can be applied +to peripherals to ensure that only certain parts of a program can modify a +peripheral. This *access control* makes software easier to reason about +compared to the alternative of treating peripherals as global mutable state.