3 ms·
You have done no more to show an actual distinction in the approach than TFA and its linked blog post... It sounds like a naming thing to me. On one side we nam
by nrds 5mo ago
You have done no more to show an actual distinction in the approach than TFA and its linked blog post... It sounds like a naming thing to me. On one side we name the term/program as a term and see it as something checked by the kernel, and on the other you name the term/program as a program and see it as something executed by the runtime. What's the difference?
- zozbot234 5mo agoThere is indeed no difference if your dependent-typing approach is using reflection (where the checked term is actually a program that's logically proven to result in a a correct proof when executed - such as, commonly, by running a decision procedure) but that's not a common approach.
- auggierose 5mo agoThe difference is that a term is not (necessarily) a program. Also checking is not executing. Its like saying riding a horse is the same as eating a fish. Really just a naming thing, what's the difference?
- nrds 5mo agoYou're drawing an equivalence between the wrong pair of things. I'm not saying that term=program; I'm saying that the type checker, qua `term -> context -> decision`, bound to a particular term, is a program `context -> decision`, and the other approach is also a program `context -> decision`. I guess it's defunctionalization, not "nothing", but a next-door neighbor of "nothing".