Makarius wrote: > I didn't know you are still planning to switch back to SML. Anyway, what > did you find nicer about OCaml?
Oh, little things in the syntax. Anonymous functions can have multiple curried arguments (fun a b -> a+b), "match" statement cases can carry more than one alternative (match x with (A n | B n) -> n-1), less indentation in the way that the let/in construct gets used as opposed to SML's let/val/in/end construct. Makarius wrote: > For the moment my main observations are: > > .... > * Still too many obvious attacks are simply declared as forbidden in the > Bounty.txt. Here is the copy from holzero-0.5.4 for the record: > > - building HOL Zero from a non-standard ML session state (e.g. with > parallelism) > - overwriting key ML objects (e.g. the 'thm' datatype or 'get_all_axioms') > - overwriting the pretty printer for key ML datatypes (e.g. 'thm' or 'list') > - circumventing the ML language proper or its type system (e.g. 'Obj.magic') > - circumventing, reconfiguring or interfering with the ML interpreter > - exploiting bugs in the ML interpreter > - changing the operating system environment in which the ML interpreter runs The immediate priority for me is to get it all written down somewhere, so that an auditor has a basis to work from. This hasn't been done before (or at least not comprehensively) for other theorem provers, as far as I am aware (and I would very much like to know if it ever has been done before). As far as convincing themselves that they can trust whatever comes out of a given theorem prover, all the proof auditor has to do is convince themselves that none of the above happens in a given proof script that supposedly establishes a given result. Once they've done that, the LCF approach means that they can then ignore the contents of the proof script and concentrate on the state of the theorem prover having processed the script (I call this "black box" proof auditing). The point of the $100 bounty is to help give assurance that the list of dodgy things catches everything. > For example, ML with parallel threads should now be standard, not > non-standard as declared above. It is merely a historical accident that > OCaml is still sequential by default. Your code will require some > additional refinements to make it thread-safe, which requires some "piling > up of more stuff". An alternative would be to nail down the environment > to be always sequential. Yes, in the future I hope to chip away at some of the items in the list, and I agree that catering for parallel threads must be a high priority one. I think I know how to do this already, but I'm a bit stretched for time at the moment to change anything fundamental. Mark. ------------------------------------------------------------------------------ Live Security Virtual Conference Exclusive live event will cover all the ways today's security and threat landscape has changed and how IT managers can respond. Discussions will include endpoint security, mobile security and the latest in malware threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/ _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
