An ongoing challenge for computer science is the development of a tool which automatically verifies programs meet their specifications, and are free from runtime errors such as divide-by-zero, array out-of-bounds and null dereferences. We have been developing a programming language from scratch to simplify verification, called Whiley, and an accompanying verifying compiler. Like other modern programming languages (e.g. Go, Rust) Whiley eschews ideas from object orientation and is perhaps most similar in style to C. In this paper, we illustrate a short example illustrating how C strings can be encoded in Whiley, and then safely reasoned about.