On Sun, 13 May 2012, Ramana Kumar wrote:
> On Sat, May 12, 2012 at 11:54 PM, John Harrison
> <[email protected]>wrote:
>
>> | Does this mean unit lists in HOL Light? :)
>> | I'm thinking of adding a check that there are no more than 2^30-1 type
>> | variables in the input theorem.
>>
>> I don't exclude either possibility yet...
>>
>
> And what about switching to big integers? (for HOL Zero and/or HOL
> Light) I thought HOL Zero might be switching to SML at some point
> anyway?
With unit list John was probably hoping to have a precise model of natural
numbers in OCaml. This is not exactly the case, because datatype values
can have loops in that language:
let rec uuuh = () :: uuuh;;
List.length uuuh;;
Anyway, I think we need to find an exit strategy from this endless thread.
Already in October 2009, I've tried to convince Mark that OCaml is not the
right vehicle for extremely high trustability that he wants to have for
HOL Zero. And back then, I did not know all these nasty tricks yet that
can be learned in the coffee room of LRI, with hardcore experts like
Filiatre showing off all the boundary cases and neat tricks outside the
normal mathematics of ML.
This is why SML never became very popular, because it spoils these games.
Makarius
------------------------------------------------------------------------------
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
