  The Rust programming language has garnered significant interest and use as a
modern, type-safe, memory-safe, and potentially formally analyzable programming
language. Our interest in Rust stems from its potential as a hardware/software
co-assurance language, with application to critical systems such as autonomous
vehicles. We report on the first known use of Rust as a High-Level Synthesis
(HLS) language. Most incumbent HLS languages are a subset of C. A Rust-based
HLS brings a single modern, type-safe, and memory-safe expression language for
both hardware and software realizations with high assurance. As a a study of
the suitability of Rust as an HLS, we have crafted a Rust subset, inspired by
Russinoff's Restricted Algorithmic C (RAC), which we have imaginatively named
Restricted Algorithmic Rust, or RAR. In our first implementation of a RAR
toolchain, we simply transpile the RAR source into RAC. By so doing, we
leverage a number of existing hardware/software co-assurance tools with a
minimum investment of time and effort. In this paper, we describe the RAR Rust
subset, detail our prototype RAR toolchain, and describe the implementation and
verification of several representative algorithms and data structures written
in RAR, with proofs of correctness conducted using the ACL2 theorem prover.
