Hacker News new | ask | show | jobs
by neel_k 3297 days ago
> I hear "dependent types" and I think "theorem prover", but it seems like Idris is a cleaned up Haskell with some light proving features built in?

It's a full-strength dependent type theory, but is intended primarily for use as a programming language. So the design focus is on using full dependent types to make ordinary programming easier.

> What's a good excuse to try Idris?

The best excuse of all: it is super fun.