> Because we really ought to go that way (more proofs like Idris/Agda). proofs are not everything in software. what do you do if you're handed a massive code-b

> Because we really ought to go that way (more proofs like Idris/Agda). proofs are not everything in software. what do you do if you're handed a massive code-base in idris and are asked to make a change, a change that requires jumping through all sorts of hoops due to the type system? constrained type systems are fine but along some vectors of software development, they actually increase brittleness. maybe not brittleness at run-time but at develop and maintenance time.