Elm is one example of such. However, it's also an illustration of why these languages are rare. With a strict semantics there's an almost unbearable temptation to add library functions with side effects. Elm only avoided this fate by giving its BDFL strict control over which packages could access the JS FFI. But that upset a lot of people.
All of them (especially newer ones) are, except Haskell (und some other, nowadays either obsolete or really obscure languages).
Idris (2), PureScript, Elm, Unison, Roc, Lean (4), Koka, Flix (and some other I've forgotten about).
Elm is one example of such. However, it's also an illustration of why these languages are rare. With a strict semantics there's an almost unbearable temptation to add library functions with side effects. Elm only avoided this fate by giving its BDFL strict control over which packages could access the JS FFI. But that upset a lot of people.
I think Idris is the best example of a pure strict-by-default language (that also supports totality checking, I believe).
> that also supports totality checking, I believe
Yes, it does. It's also dependently typed.
PureScript is an example.