Comment by kccqzy

I would’ve expected that people who like computers will converge around something like Idris. It’s marketed as a development tool, not a tool for formalizing mathematics even though it could be used as a proof assistant.