Comment by dhbradshaw

I'd argue for moonbit -- faster compile times, almost as fast, smaller wasm artifacts and like lean can have proof of correctness built in.