On Fri, Jul 4, 2014 at 2:01 PM, Jonathan S. Shapiro <[email protected]> wrote: > On Thu, Jul 3, 2014 at 4:04 PM, Geoffrey Irving <[email protected]> wrote: >> >> I hope that system languages get to dependent types long term, but I >> frankly don't think they are practical without some heuristic theorem >> proving support, which is much worse in terms of compiler dependence >> than a time cutoff. That probably rules them out for bitc. > > I'm somewhat on the fence about this. In the large, I think you are right.
Then you're probably going to have a similar objection to my idea of heuristic effect polymorphism inference. In certain systems, the two forms of compiler heuristic magic can actually be unified. > One way to resolve this is to define a standard search algorithm and search > resource environment that all compilers must implement. That gives us a > place to stand to define portably compilable programs, which is the thing we > actually need here. We can then introduce a syntax for proof checks and let > more advanced provers emit their proofs in checkable form for inclusion into > the source text so that the reference algorithm can validate proofs that it > cannot produce by itself. This is somewhat like the approach taken by Coq, where there's a kernel type checker, and a bunch of relatively unstable machinery on top to build the fully explicit terms. The thing to be wary of is that when the difference in smarts between the levels gets too big, it becomes easy to have certain styles where a small increase in the code for the smart level results in a huge increase in the size of the explicit terms that get dumb-checked. This is one of the main two scalability issues Coq has, I'd say. And Coq doesn't have a good all-around solution to this because the closest thing, proof by reflection, runs right into the other scalability issue, which is nonexistence of good algorithms for certain functions, due to strong normalization. _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
