We already have this in things like `Arbitrary` type classes, `QuickCheck`, `Hedgehog`, etc.. Hundreds of automatic test cases generated so that you don't focus only on "I thought of these 5 test cases" type of testing.
There is a PureScript compiler called `purerl` for the BEAM which can be used to write BEAM code in a ML derivative. It works and I personally would use it if I had to deliver BEAM code next week. For the most part it's the answer to the "you can only write BEAM code in bad languages" issue.
Maybe in a very strongly-typed language, but having used a pretty wide variety of statically-typed languages, I can confidently say none of them had strong enough type systems that the assertions made by the type system could be considered "comprehensive". You still need a test suite.
Static languages fell out of favour last time round the dynamic/static merry-go-round because the typing started to get in the way. You ended up writing more type boilerplate than actual code - and not breaking your methods/functions down into smaller functions to avoid having to write out even more type boilerplate.
I often wonder whether type annotations that allow a processor to generate tests that can integrate into your test suite would be a useful thing to have. Sort of like a C preprocessor.
Then you could add ML type headers to Elixir functions and get a set of ExUnit tests back.