On Thu, 3 May 2012, Freek Wiedijk wrote:
> This is not very much about HOL as such, so if this reply is
> inappropriate for the HOL list, I apologise:
I am also a guest here, so we try to behave as best as we can.
>>> mutating the names of constants.
>
> I always found this "mutable constants" complaint silly. Many people
> make it, but it never struck me as significant.
The question is what is the name of the game you want to play. Mutable
term language is not quite "LCF approach", where the static type
discipline is supposed to ensure "correctness-by-construction".
For HOL-Light, John always keeps an eye on his sources -- static check by
human inspection. The ACL2 guys also manage that by hand in their weakly
typed language, by restricting the number of people who work on the
code-base to two. For a huge system with many contributors you can't do
that. This is where a robust LCF approach really helps.
Mark Adams occasionally promotes an even more aggressive scenario for HOL
Zero where he wants to admit potentially malicious users, an army of paid
proof-workers who want to cheat. (I am not really following him here, we
are not that far yet.)
> Surely in every practical programming language you can "cheat" in some
> way if you try hard enough. For instance by poking the memory, either
> internally through some Obj.magic like interface
This Obj stuff is absent in SML. You can make nonsense with some
implementations, but we reduce that danger by running with more than one,
so it is essentially the intersection of the semantics.
Moreover, as I have explained to Mark Adams already in a similar
discussion, one can seal up the toplevel interpreter loop, to isolate user
scripts from any such built-in nonsense. I think the original LCF by
Milner actually did work like that, since ML was a closed interpreter
within LISP. (Unfortunetely, I've only ever seen the sources of Cambridge
LCF. Does anybody happen to have the older ones from Edinburgh or
Standard?)
A managed ML toplevel is again one of these layers that would complicate a
prover implementation, but make it more reliable. We don't have that in
Isabelle, because the malicous scenario is a bit artificial, but there is
some runtime compiler support to allow the user to work with ML bindings
in a stateless manner.
> or if you don't get that from your language by poking in /dev/mem?
That's another game. A computing system consists of many layers. If you
have full physical or logical access to critical ones, you can do whatever
nonsense you want.
Milner had some very important ideas in the 1970-ies how to organize the
chaos, such that you get mostly real theorems out of it -- by restricting
to certain layers, and some infrastructure to enforce that.
> What's important is that you won't "cheat" accidentally, by
> misunderstanding how things work.
I've recently made my first practical steps in OCaml and was a bit scared
by its proximity to C. After 20 years of SML I am probably spoilt by too
clean programming language semantics.
I did "cheat" by accident, stumbling over standard semantic traps of
low-level languages. Most languages have that, but it does not mean one
cannot do better.
Again, these oberservations are more relevant to a project like HOL Zero
than for HOL-Light. I've looked at holzero-0.4.1 before and just today at
holzero-0.5.4. (I am still hoping to see a really convincing independent
proof checker for the HOL family of systems.) My impression is now that he
*is* piling up more and more stuff to make up for the semantic weaknesses
of OCaml for his project.
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
