Yes, a strong argument, and staying in a line of PLs: F# for high-level, and F* <-> Low* for theorem proving and low-level coding. I am evaluating F/Low for verified code on Cortex M processor that I am currently trying to write SPARK2014. The Cortex A processor is running seL4 for less safety-critical tasks. I did look at Lean4 as a scratch for my Idris2 itch use cases.