On Fri, Jul 4, 2014 at 11:01 AM, 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. > 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.
Checking in proofs is clearly the "one true way" to handle this long term. If bitc does go the dependent type route, it may be worth baking this idea into idiomatic usage form the start to make extensibility easier down the road. On the other hand, the fact that a third party compiler is guaranteed to check and compile source + generated proof doesn't mean that it's guaranteed to be able to extend the same even in trivial ways. Dangers would still lurk. Geoffrey _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
