Discussion
I view types as "manifestly obvious properties". It is important to me that checking them is decidable in practice. That would suggest the typechecker should be cautious when provoked to run programs. Totality is the minimum acceptable level of caution. It's not where we're going. That we aren't there yet is no argument against going in that direction.
The "what if it's not actually looping, just Ackermann?" crew have a point, but it's not a point against totality.
As far as dependent type theories are concerned, I see them as languages of checkable explanations. If checking the type requires further explanation than was present in the syntax of the subject, then the subject was not in itself an explanation. It might be a realiser or something, but such systems have left behind the business of furnishing cogent documents.
The reason I am an intensional type theorist is that I use computers. I want the means to negotiate the division of labour between humans and computers in a way which is precise. I have no truck with either explicable drudgery or inexplicable magic. That which is systematic should be a system. That which is not systematic should not be a system.
I live by the perspicuous effectiveness and good taste of the disappointing accidents I choose to engineer. Philosophy alone will not tell us what to do.
Install bonfire.cafe
Get the full app experience
