Learning about Shen is what inspired the project for me. Combination of sequent calculus and prolog in a highly portable lightweight kernel that is easy to port to many runtimes (https://shen-language.github.io) gives a ton of expressive power. If you only want compile-time checks, plenty of other notations work. What actually interests me is the possibility of a single spec whose invariants produce enforcement that crosses compile time (guard types + shen tc+) and runtime (generated checks in constructors, plus the spec itself as a test oracle via shen-derive), with no translation layer required between them.