I reviewed some of these programming languages in the past. LEAN (sometimes spelled L∃∀N) made my list and got some attention but you left it out. Idris and Coq caught my eye, and I chose to explore Coq more for reasons of ecosystem maturity.
But when I tried to do almost ANYTHING in Coq I found the going very very very slow. Like.. the law of excluded middle isn’t in there by default, which I discovered after hours of painful debugging attempts on an early exercise (proving the infinitude of primes) that I thought would be fast.
Do you have a favorite? Do you know of good tutorials for that favorite?
I reviewed some of these programming languages in the past. LEAN (sometimes spelled L∃∀N) made my list and got some attention but you left it out. Idris and Coq caught my eye, and I chose to explore Coq more for reasons of ecosystem maturity.
But when I tried to do almost ANYTHING in Coq I found the going very very very slow. Like.. the law of excluded middle isn’t in there by default, which I discovered after hours of painful debugging attempts on an early exercise (proving the infinitude of primes) that I thought would be fast.
Do you have a favorite? Do you know of good tutorials for that favorite?