With the mainstream programming languages now including the likes of Rust, type systems reasoning about ownership have regained attention over the last few years. Fundamentally, ownership allows the programmer to reason about aliasing, and using this knowledge to reason about side effects. In the Verona project, we believe mutation is a fundamental way in which programmers think about programs. In the context of the Verona programming language, we are exploring how mutation can be constrained to support reasoning about ownership giving rise to useful properties, both from the perspective of automatic memory management and concurrency. In this talk, I will explain some of the technical challenges of designing a language with ownership built in. From type system details, e.g. subtyping, to implementation.