On Mon, Jul 7, 2014 at 3:30 PM, Matt Oliveri <[email protected]> wrote: > 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.
I think so, since "checking in proofs" in this context means checking them into a version control system (I was agreeing with shap). If you're responding to specific language in a post it's better to reply below the quoted paragraph, by the way. > 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.) I'd be very curious to hear it. Maybe another thread unless shap thinks we've veered out of bitc territory? This one about grammar is getting a bit long. Geoffrey _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
