Introduction: residency is a binding attribute

Miri does not have a separate "GPU array" type. An Array<f32, 4> is the same type whether it lives on the host or the device — what differs is the binding's residency. Residency is an attribute on the binding, exactly like mutability:

let  x = [1.0, 2.0, 3.0, 4.0]      // host-resident, immutable
var  y = [1.0, 2.0, 3.0, 4.0]      // host-resident, mutable
gpu let a = [1.0, 2.0, 3.0, 4.0]   // device-resident, immutable  (uploaded)
gpu var d = [0.0, 0.0, 0.0, 0.0]   // device-resident, mutable

Two axes — mutability (let/var) and residency (host/gpu) — give four binding forms and zero new types. The gpu keyword is the only source of device residency. Reading any file, grep 'gpu let\|gpu var' enumerates every device-resident binding.

Here is a complete GPU program — two arrays added element-wise on the device:

use system.gpu
use system.collections.array

const N = 4

gpu let a = [1.0, 2.0, 3.0, 4.0]
gpu let b = [5.0, 6.0, 7.0, 8.0]
gpu var dst = [0.0, 0.0, 0.0, 0.0]

forall i in 0..N
    dst[i] = a[i] + b[i]

let host = dst
println(f'{host[0]} {host[1]} {host[2]} {host[3]}')

Output: 6.0 8.0 10.0 12.0. Five lines of GPU logic. The CUDA equivalent is roughly forty. Save it as add.mi and run it with miri run add.mi — that's the whole workflow.