4 ms·

I think that when you have a type system that catches all bugs the type system itself is probably Turing complete. Writing the types in such a system may very w

I think that when you have a type system that catches all bugs the type system itself is probably Turing complete. Writing the types in such a system may very well be programming. The more advanced systems are already too hard to use too be helpful for common business people which means they don't help much in reducing bugs from misunderstanding the specs. Just my $0.02.

lmm 9y ago
> I think that when you have a type system that catches all bugs the type system itself is probably Turing complete. Writing the types in such a system may very well be programming. It is programming (though the best way to do it is in a system that's distinctively not Turing-complete - look at what Idris does), but it's all verified at compile time. > The more advanced systems are already too hard to use too be helpful for common business people which means they don't help much in reducing bugs from misunderstanding the specs Not my experience. The type systems make it much easier to express your actual business logic in straight-through code that looks like what it's meant to do, shunting off the awkward cross-cutting concerns to be resolved ambiently in a way that's safe, but doesn't get in the way right now.