One can just use Lean4 and panic each time it asks proof. 5 of 5. Community is PhDs and geniuses. Types are values, full uniformity = simplicity. Perf > Swift because reference counters eliminated at compile time. AI likes types. Just panic when Lean4 asks for proofs. Backed by biggest corps out there. Macro are best of Rust and Scala.