Comment by ggleason

If you write it in a theorem prover you can have the LLM write proofs about the code quite easily. Lean is easily good enough to compete with javascript, so now I think it makes sense to switch to Lean.