I agree on the beauty of liquid types. I encourage HN to learn Sail, simply to get experience with liquid types. The Sail specification of RISCV is currently the only place where liquid types are used in industrial code. (There is Liquid Haskell and Liquid Rust, but they are research prototypes.) I expect that over the next decade or two, liquid types will come to the programming mainstream.
The configurability problem has several main parts.
(1) It's a Turing complete problem as the informal RISCV specification gives you so much freedom, including all those IMPDEFs. The specification of a complex, configurable ISA will always be intrinsically complex and syntax can only do so much about presenting this intrinsic complexity.
(2) Sail's lack of a clear, easy to use module system for configuration of the exact RISCV version to be emulated.
The configurability problem has several main parts.
(1) It's a Turing complete problem as the informal RISCV specification gives you so much freedom, including all those IMPDEFs. The specification of a complex, configurable ISA will always be intrinsically complex and syntax can only do so much about presenting this intrinsic complexity.
(2) Sail's lack of a clear, easy to use module system for configuration of the exact RISCV version to be emulated.