[mapcars]

Proof of correctness would be fantastic, but I have yet to see it in action. LLMs maybe could do it for simple program, but I'm pretty sure it will fail in large codebases (due to context limits), and types help a lot in that case.

> for "explorative computing", proof-of-concepts, RAD or similar that tends to get in the way

I would even argue that its better to have typed system even for POCs, because things change fast and it very often leads to type errors that need to be discovered. At least when I did that I often would do manual tests after changes just to check if things work, with typing in place this time can also be minimised.