Sail is not at the register-transfer level (RTL) [1].
Why? Because
Sail does not offer abstractions for clocked digital circuits, which is what characterises the RTL. The most widely used DSL for the RTL is (System)Verilog [3].
Instead, Sail is a stand-alone DSL for the ISA (= instruction set architecture). The purpose of the ISA level is to talk about that a processor looks from the outside, to the programmer (most specifically to the compiler writer). Sail is a minimal programming language with a single purpose: writing ISA specifications, which means writing an interpreter for assembly language.
Technically, Sail is a simple imperative language with first-order functions. What makes Sail suitable for specifying ISAs is its typing system. Sail supports
types that are frequently used in ISA interpreters, such as dependent typing for numeric types and bitvector lengths. Sail is closely related to Arm's ASL (= architecture specification language) [2].
Since Sail is Turing-complete, any ISA can be modelled, including Mill. For the same reason any RTL can be modelled, for example by coding up an interpreter for an RTL language like Verilog, but that would be mighty inconvenient.
I see now where the confusion comes from: the abbreviation RTL is overloaded to (1) register-transfer level (as e.g. Verilog) and (2) register-transfer language (e.g. GCCs intermediate representation you cited). I think the former use is much more widespread. I agree GCC's register-transfer language is close to Sail.
Why? Because Sail does not offer abstractions for clocked digital circuits, which is what characterises the RTL. The most widely used DSL for the RTL is (System)Verilog [3]. Instead, Sail is a stand-alone DSL for the ISA (= instruction set architecture). The purpose of the ISA level is to talk about that a processor looks from the outside, to the programmer (most specifically to the compiler writer). Sail is a minimal programming language with a single purpose: writing ISA specifications, which means writing an interpreter for assembly language. Technically, Sail is a simple imperative language with first-order functions. What makes Sail suitable for specifying ISAs is its typing system. Sail supports types that are frequently used in ISA interpreters, such as dependent typing for numeric types and bitvector lengths. Sail is closely related to Arm's ASL (= architecture specification language) [2].
Since Sail is Turing-complete, any ISA can be modelled, including Mill. For the same reason any RTL can be modelled, for example by coding up an interpreter for an RTL language like Verilog, but that would be mighty inconvenient.
[1] https://en.wikipedia.org/wiki/Register-transfer_level
[2] https://alastairreid.github.io/ARM-v8a-xml-release/
[3] https://en.wikipedia.org/wiki/Verilog