Who said anything about making a trade-off? I wasn’t proposing to take anything away.
Also, I was talking about “agda” with an extra g, which is not the same as ada. It uses proof by reflection, which Julia might be able to do if it had some extra inductive type features.
The new features don’t have to exactly resemble a previous language, just learn from it.
Are inductive types threatening to other aspects of the Julia language that would cause trade-off?