>>10951696>What is it used for, and why should I choose Idris over other languages?>>10951696>What's the advantage of this?the bad
under developed
difficult
the good
Interactive type checking
theorem proving
>u already know what that is>create natural transformations from data to derived types dependent types
example just say you're modeling a projectile
each state of the projectile could be a dependent type.
state aware systems. currently neural nets are not state aware
It's the missing link the AGI
