I've received a description of how HOL ensures soundness from its maintainer. The core issue is whether Scheme can enforce abstraction boundaries for abstract data types. I think that's what the sealedness and opaqueness of records is for, right?
On Thu, May 28, 2009 at 6:44 AM, Ramana Kumar <[email protected]> wrote: >> I wonder why not *apply* these interesting and generalized Scheme >> discussions to the comp.lang.scheme newsgroups? > I've CC'ed comp.lang.scheme. > >> Anyway, I think you're confusing static and dynamic type checking. >> Sure it's possible to write theorem provers in pure R5RS Scheme by >> relying on predicate functions and dynamic type checking. I think the >> so-called soft-type checkers for Scheme were like that -- they are >> theorem provers trying to validate a scheme program as input (supposed >> theorem). > Would you need records, though? Otherwise what would you "theorem?" > predicate look like? Or wouldn't you need such a predicate? > >> Besides, I don't think records in Scheme are all that static, at least >> not if not truly builtin. > I'm not sure whether I care about the static/dynamic difference... > mostly because I don't know the tradeoffs. Presumably you can be > faster if you're static. The proposal I made of hiding the privileged > constructors of a theorem record in a library wouldn't amount to > adding static type checking to Scheme at all, but it might be a way to > guarantee the soundness of the theorems without any overhead compared > to ML. (I might be wrong... let me know.) > >> >> On Wed, May 27, 2009 at 5:02 PM, Ramana Kumar <[email protected]> wrote: >>> Interactive theorem provers like HOL and Isabelle use the static type >>> checking in ML, where type safety is guaranteed, to guarantee >>> soundness. Specifically, something of type "thm" (for theorem) must be >>> true, because (I think this is how it works) only the axioms and >>> inferences rules produces things of that type. At the same time, these >>> systems are very extensible and you can write more powerful inference >>> rules or functions that return theorems in ML... the type system >>> ensures that the only way these functions can work is by proving their >>> results, i.e. calling the low level axioms and rules. >>> >>> Now I've been thinking about whether one could write something like >>> HOL in Scheme. At the moment I'm thinking you could put the kernel >>> (the axioms and inference rules) in a library along with a new theorem >>> record type, and then not export any method for creating theorem >>> records that isn't an axiom or rule. Would that guarantee soundness in >>> the same way, or can you never really restrict how records of a type >>> are created? Also, is it possible to do it without records or >>> libraries (e.g. in R5RS)? Finally, let me know if there already exist >>> theorem provers written in Scheme. >>> >> >
