We present on-going work of a shallow embedding of an array programming languages using F* and Pulse. Our work focuses on addressing the technical challenges regarding compiling a static rank polymorphic language to GPUs. The challenges are two-fold: 1) proving array operations that use constant memory allocations, and 2) making proofs about such programs more ergonomic in concurrent separation logic.