Software compiler engineers target ISAs so that compiled machine code can run on a common platform and is correct and as efficient as possible. On the other hand, hardware engineers target ISAs so that their processors can support certain classes of software. This separation of duties is problematic because it deepens the difficulties of verifying correctness from compiled code down to its hardware. We see an opportunity to alleviate these concerns by automating this passage from ISA to hardware. The challenge is that verification and automation tooling for ISAs and hardware description languages (HDLs) have tended to treat implementation effects, such as state, exceptions, and non-determinism, in a variety of different ways, not to mention, these tools can be spread across the imperative/functional language spectrum. By concentrating on tools which originate in the functional programming space, we observe that a simple (unoptimized), functionally correct hardware implementation for a processor may be derived in a straightforward manner from the ISA’s formal specification. We propose a proof of concept for translating formal ISA specifications to valid hardware implementations, e.g. in Verilog, in a single software pipeline.