I tried recommending proof checking, rather than type checking, as the proper foundation of a safe system, on this list back in 2012. It didn't go over very well at all. In hindsight though, I did a pretty lousy job trying to explain the motivation. But the idea was indeed that it would be more extensible.
But maybe I'm misunderstanding you. Anyway, I have an idea about how to avoid the limitations of a fixed "official" proof checker. It's what I've been thinking about since then. It's overkill though, given that BitC is just dabbling with dependent types. (Or at least that's my understanding.) On Mon, Jul 7, 2014 at 4:26 PM, Geoffrey Irving <[email protected]> wrote: > 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. _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
