Hi Makarius, | * Standard ML with its no-sense semantics
This reminds me that last time I looked at SML (which was admittedly a long time ago) the formal semantics left integer arithmetic almost completely undefined, and at least one implementation used machine arithmetic. Has that situation now changed? I agree that mutable strings are indeed a gross misfeature of OCaml. I think even Xavier might concede as much; at least, last time I whinged to him about it he didn't actually demur but just explained how the design came about. I have sometimes thought about using my own pet string type in HOL Light, as Mark has done in HOL Zero, but resisted the slight uglification of the code, an example of exactly the kind of dilemma between simplicity and security that you mentioned. Note that F# has immutable strings and is otherwise pretty close to core OCaml, and it seems to be getting quite popular. I'd use it more myself if it were a bit more Linux-friendly, and I have the idea of porting HOL Light to it there in the back of my mind somewhere. I think the code for my theorem proving book would be an easier first step, though. John. ------------------------------------------------------------------------------ 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
