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. Not least because there are many search strategies for provers, and two different implementations of the compiler might use two different search strategies as part of their competitive differentiation. And also because *changes* to search strategies that generally improve version k+1 of the compiler might cause correct programs in version k to cease to compile. 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. shap
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
