# Ghost code vs. exec code The purpose of `exec` code is to manipulate physically real values --- values that exist in physical electronic circuits when a program runs. The purpose of ghost code, on the other hand, is merely to *talk about* the values that `exec` code manipulates. In a sense, this gives ghost code supernatural abilities: ghost code can talk about things that could not be physically implemented at run-time. We've already seen one example of this with the types `int` and `nat`, which can only be used in ghost code. As another example, ghost code can talk about the result of division by zero: ```rust {{#include ../../../../examples/guide/modes.rs:ghost_abilities0}} ``` This simply reflects the SMT solver's willingness to reason about the result of division by zero [as an unspecified integer value](https://microsoft.github.io/z3guide/docs/theories/Arithmetic/#division). By contrast, Verus reports a verification failure if `exec` code attempts to divide by zero: ``` error: possible division by zero | | let y = x / 0; // FAILS | ^^^^^ ``` Two particular abilities of ghost code[^note_tracked] are worth keeping in mind: - Ghost code can copy values of any type, even if the type doesn't implement the Rust `Copy` trait. - Ghost code can create a value of any type[^note_uninhabited], even if the type has no public constructors (e.g. even if the type is a struct whose fields are all private to another module). For example, the following `spec` functions create and duplicate values of type `S`, defined in another module with private fields and without the `Copy` trait: ```rust {{#include ../../../../examples/guide/modes.rs:ghost_abilities1}} ``` These operations are not allowed in `exec` code. Furthermore, values from ghost code are not allowed to leak into `exec` code --- what happens in ghost code stays in ghost code. Any attempt to use a value from ghost code in `exec` code will result in a compile-time error: ```rust {{#include ../../../../examples/guide/modes.rs…