On Thu, 3 May 2012, John Harrison wrote:
> Of course, the ability to understand a system down to the bottom does
> have real value for those whose intended use is a bit more radical and
> outside the normal or expected usage model. Besides, I think many people
> are interested in formalization precisely because they want to have a
> clearly understood foundation, a kind of "search for certainty". So
> those who are naturally drawn to formalization in the first place may
> also appreciate being able to understand completely the logical and
> software engineering foundations of a system.
This is a delicate and very interesting aspect.
A system like HOL-Light has the advantage that the reader gets quickly an
impression what the basic logic functionality is meant to be. This gives
some certainty under additional assumptions, i.e. that the ML really is
what it seems at first sight, and that certain bad things are not done in
practice. (Say someone taking apart terms and mutating the names of
constants.)
When Mark Adams showed his new HOL0 system for in Cambridge in 2009, he
did not know yet about these snags of OCaml. Both type int and string are
somehow insecure on this platform. I've also done a tiny bit of OCaml
implementation myself some weeks ago, and had to look a few days very
closely what the basic operators mean, say equality on strings.
Sealing up such holes makes the implementation more complex. For example,
the Coq people have their own version of int and string that really mean
int and string in a mathematical sense, without silent overflow or hidden
mutation.
Driving this further and further, adding infrastructure to address
weaknesses of the implementation and other side-conditions, you get to a
highly complex system like Isabelle. Here the idea is to provide a secure
and fast environment to the end-user, like an operating system does, but
the first impression that one could easily understand it is lost.
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
