"Frode Vatvedt Fjeld" <fro...@acm.org> wrote in message
news:2hadtikgpb.fsf@vserver.cs.uit.no...

You were arguing that proof-carrying code, or
trusted-compiler-generated code was not an adequate replacement for a
user/kernel barrier (and concomitant user/user process barriers).  It
seemed to me that you were saying that was because you wouldn't be
willing to actually trust the compiler or the proof-checker to do a
perfect job, and so it might let in things that shouldn't be let in.

My reply is that your "hardware" solution actually still depends on
the compiler's ability to correctly compile the kernel code (and not
generate stray memory writes that might clobber page tables, for
example).  It also depends on your ability to read through the
page-table handling code, and verify that it really does enforce the
required barriers.  It depends on there being no errant code
(anywhere!) in the kernel which might execute a stray memory write
that happens to clobber a page table.

So you are really trusting quite a lot.

A proof-checker is pretty easy to get right.

Moreover, a trusted-compiler is just like any other compiler.  That
is, when I trust the trusted-compiler not to generate stray memory
writes, I'm doing *exactly* the same thing as when I trust whatever
compiles the kernel not to generate stray memory writes.

    Because I can't lay my hands on any other kind.  The only kind of
    native code I'd regard as trusted is that for which there is a formal
    correctness proof.  Since I can't get an X server or a Lisp system
    which has such a proof for instance, I'm constrained to run ones which
    might follow random pointers occasionally.  In order to reduce the
    damage that this kind of problem does I like to have a whole lot of
    dynamic checks on things.

If you are running traditional process/kernel programs, they may well
rely on such protections (even if inadvertently).

The discussion is, however, focused on new systems--ones which, for
example, might have no process/kernel split.  Or, for example, adding
extensions to existing well-designed systems.

Why do you want a formal proof for a Lisp system before you accept its
pointer guarantees, but you don't expect a formal proof for the C
compiler or your kernel, before you accept their guarantees?

In article <y6csn7a7tcx....@octagon.mrl.nyu.edu>, Marco Antoniotti

  You are arguing against ludicrous and bogus arguments you have imputed to
  me, but which I have not expressed, implied, or made it possible to infer
  in the first place.  _That_ was what was wrong, not your "argument".  I
  have extremely low tolerance for people who play rhetorical games where
  the goal is to embarrass someone instead of actually making a point, and
  if you engage in gratuitous fault-finding, too, there is no good-will
  left on my end at all.

In particular the following product:
http://www.polyspace.com/product_datasheet/cverifier.htm

Yes, I know, it's for C and (to my own astonishment) they use abstract
interpretation (an obscure method, even statically typed people not
necessarly like) and no, of course, they do not detect *all* errors at
compile time as they claim, but they give the developer the opportunity to
prove certain properties or narrow down potentially buggy parts (and this
provably correct!) So, I can imagine that combining such a tool with
computer guided (human) theorem proving may actually get you a bit closer
to an all provably correct OS.

Btw, they seem to have a whole bunch of customers who *are* actually be
interested in provably correct products:
http://www.polyspace.com/references.htm

Kind regards,

Your definition of "untyped"-ness also reveals a definite "static"-outlook,
which is a different view than that taken by Lispers.  In the static
view (which I am not condemning), there are distinct and separate phases
for compilation and execution.  As a result, no changes may be introduced
into the running program and the consequence is that compile-time type-
invariants are held.  Thus it is possible to claim that a program which
has a type-error must've been programmed in a language that did not
distinguish between types (which "untyped" implies to me) because there is
no way to make further changes that rectify the error.

In the "dynamic" view that Lisps generally favor, there is no time set
aside only for compilation and no time set aside only for execution.
Since it is quite possible to merge newly-compiled code into an already-
running image, the language and compiler needs to accomodate the fact
that at some point in the process the type-invariants may be broken
(even if it is only temporarily).  The solution to this, while preserving
the dynamic nature of Lisp, is the excellent condition system found in
CL, which allows you to work with the system even in an "exceptional"
state.  No longer is it possible to claim that a type-error implies
untyped-ness, because it is the nature of the system that incremental
updates may break certain invariants.  A "type-error" means that the
system is in fact performing type-checking and distinguishes between
types, which would be a rather odd thing to be called "untyped".
Furthermore there is a strong sense of object-identity in CL which is
linked to "strong" type-checking.

Please do not confuse "dynamic" with "weak" or "untyped".  There are more
points of view than the static one out there, and some of them suit
certain problem-sets better than others.  There are even languages which
can be considered to be static and weakly typed, such as C.  I find the
two criteria to be orthogonal.

My training in philosophy sometimes gets ahead of me, I'm afraid.
When confronted with a proposition that I believe to be false, I find
the clearest most direct counterexample; the goal is never focused on
the person, but only on the proposition.  And I don't have any
intention of belittleing someone or scoring rhetorical points; I'm
actually a very issue-focused person.  But that tends (again) to get
ahead of me at times, and people interpret my zeal to demonstrate the
falisty of some proposition as a zeal to demonstrate the foolishness
of some other person.  But that is never my goal--though I grant that
it can be near impossible to tell.

So this is a plea for good will.  In the particular case, I was trying
to augment the previous poster's example, the point being that
hand-typed tables can be maddeningly hard to get right at times, and
even harder to find bugs in than normal code.  I once had such a case
in (IIRC) a table of parities for ascii.  There was a bug in one of
the values, and it was so hard to notice in the midst of a big table,
that (once I found the bug) I immediately replaced it with a table
programmatically generated on startup.  *That* I could be sure was
correct.

In the instant case, however, my message was even worse, given the
presence of a foolish carelessness in my part (since, of course,
omitting the "I" was part of the original problem statement).

"Frode Vatvedt Fjeld" <fro...@acm.org> wrote in message
news:2h6646kclu.fsf@vserver.cs.uit.no...

  But has anyone actually asked for a formal proof for a Lisp system?

  Mostly, what I have written and what I understand Tim to be writing is a
  resounding rejection of all the wild claims made by the "proof" and
  "static typing" crowd, namly that such tactics at the source level is
  _sufficient_ to ensure a bug-free and fully operationsl system, and that
  is only necessary because of their attacks on the infrastructure upon
  which we rely today for problems that very few of us believe would go
  away with all that fancy-schmancy type-based proof cruft, which has a lot
  of theoretical values in how to design and not to design software, but
  those crowds are so incredibly snotty about their "superior" theories and
  so absolutely clueless about many real-world issues that simply do not
  fit their theories, and which therefore appear to many to be a case of
  "if the theory does not fit, you must acquit", which so many people who
  have "good theories" resort to in order to purposefully discard those
  parts of reality that are not explainable by their theories.  I mean, I
  know some really smart people who have these incredibly ludicrous ideas
  about how to design and run societies because they flat out refuse to
  believe that bad people exist, and so completely ignore the threat they
  pose and offer no way to deal with anyone who would seize the opportunity
  to do someone harm.  My theory of society-building is that people are
  only polite and friendly and can work together because there are some
  very serious and credible counter-forces that would be applied against
  any real or attempted use of force to begin with, and that translates to
  how computers have to deal with all of those malicious people who do
  _not_ perceive a credible counter-force to their destructive intents and
  to all those _mishaps_ that just happen to software in a very unfriendly
  real world.

ciao,
Jochen

I think the point is that proof carrying code, or using only
pointer-safe languages, obviates the need for memory barriers between
programs.  It certainly doesn't obviate the need for other security
and reliability techniques.

  However, the space of things that are the negations of falsehoods is
  rather large and does not at all need to include any truth.  By picking a
  particular negation of a falsehood, you imply that your angle on what is
  false is sufficient to construct a counterexample.  This is generally not
  true.  When somebody is opposed to something, as is the case here, there
  is no telling what they actually would like propose.  By choosing some
  counter-example to a negative argument, you actually do impute intention
  and opinions about what a person would propose if they did not oppose
  your particular argument to begin with.  I have a very hard time seeing
  how this can _not_ result in hostilities.

| But that tends (again) to get ahead of me at times, and people interpret
| my zeal to demonstrate the falisty of some proposition as a zeal to
| demonstrate the foolishness of some other person.  But that is never my
| goal--though I grant that it can be near impossible to tell.

  If someone spends a lot of time demonstrating the falsity of something a
  person does not even express or imply, because the falsity you perceive
  is in your view a counter-argument to your position.  It is vital to keep
  track of positive and negative propositions and arguments in order to
  make this work.  Because the disproportionally larger space of a negative
  proposition, the negative of a negative may not even include the positive
  -- and that means that you must be very careful in countering arguments
  against your own position with counter-examples.  Instead, support your
  initial position.

| So this is a plea for good will.  In the particular case, I was trying to
| augment the previous poster's example, the point being that hand-typed
| tables can be maddeningly hard to get right at times, and even harder to
| find bugs in than normal code.

  However, it was not hand-typed.  Christ, give me a break.  First, if it
  were a hand-typed table, the line with l-p would not _all_ be lowercase,
  now, would it?  Second, just because something is in source form does not
  mean it was typed in by a human being.  It is far easier to read a case
  statement that actually contains the cases than code that builds a hairly
  table.  It is also far better to let the compiler writers worry about the
  optimization of table lookup than to do that grunt work yourself.  case
  is the right tool for the job.

  Of all the languages in which you can write code, the Lisp family offers
  the best way of all to produce some output and recycle it as code.  I do
  this a lot, because it is often easier to write Emacs Lisp code to write
  code for you than it is to type it in manually, anyway.

| I once had such a case in (IIRC) a table of parities for ascii.  There
| was a bug in one of the values, and it was so hard to notice in the midst
| of a big table, that (once I found the bug) I immediately replaced it
| with a table programmatically generated on startup.  *That* I could be
| sure was correct.

  Well, I prefer to produce source code in intimate cooperation with the
  editor, Emacs.

| In the instant case, however, my message was even worse, given the
| presence of a foolish carelessness in my part (since, of course,
| omitting the "I" was part of the original problem statement).

  I think your careless assumption that it was hand-typed should have been
  amply refuted by the presence of a systematic error that should unlikely
  have been made by hand.

(Incidentally this is the general flaw in the `why do you trust this
thing and not that thing' argument.  If `this thing' is a library or
kernel which is used all the time and `that thing' is several hundred
programs, then it is completely rational to trust this thing more than
that thing.  It's the reason why when my Lisp programs die, I tend to
assume that I've made a mistake rather than the compiler is buggy.
Statistics is a wonderful thing, although something alien to the `discrete'
CS mindset I realise.)

-dan

--

comp.risks is next door.

And another point I made long ago /still/ remains:  If people think
we need statically typed languages to write working software, because
there provably won't be any runtime type-errors [1], why not go
all the way and demand Haskell?  Look into your mind and answer
yourself why you wouldn't write an OS in Haskell and you are
almost there:  You'll suddenly see why Lisp people don't use
statically typed languages :-)

Oh, and look at this:

(defun first-two (list)
  (list (car list) (cadr list)))

(defun start-program (program &rest args)
  (handler-case (apply (symbol-function program) args)
    (type-error (cnd)
                (format *error-output*
                        "~&~A was shut down because of a type error:~&~A"
                        program cnd))))

BLARK 7 > (start-program 'first-two 42)
FIRST-TWO was shut down because of a type error:
42 is not of type CONS.
NIL

BLARK 8 >

See?  Why couldn't my OS do just that?  No weird things happen,
no BSOD, no kernel panic.  Aren't there any exceptions you
might forget to catch in *ML?

[1] As if those languages didn't contain undocumented loopholes that
    let you circumvent that security; read the OCaml list and learn
    that advanced users of OCaml use them all the time.  I always
    have to laugh when I see that.

Regards,
--
Nils Goesche                          PGP key ID 0x42B32FC9

  You will not magically get rid of them only because

The exception thing is also a program design problem -- and those don't
get magically resolved by switching over to a statically typed language
alone.  What the language gives you is a set of tools that enable you to
redesign the problem.

Simple example:  I have a finite map data structure.  Should lookup raise
an exception if the item to be looked up is not in the domain of the map?
Well, I prefer to have lookup return an option.  This is sometimes less
convenient to use, but it makes it clear at the type level that  one must
somehow be prepared to deal with the failure case.  (Of course, in
certain applications the other interface is more convenient.)

[snip]

        #!/path/to/interpreter [arg1 [arg2 ... ] ...]

format?

Regards,
--
Nils Goesche                          PGP key ID 0x42B32FC9

Seriously, most uses of the type system I saw in *ML languages are to
define "sublanguages".  Here is an example from a Type Checker written
in very standard (AFAIU) SML/NJ

datatype Expression = constant of Constant |
                      variable of Variable |
                      lambda of Variable * Expression |
                      conditional of Expression * Expression * Expression |
                      application of Expression * Expression |
                      let_exp of (Variable list) *
                                 (Expression list) *
                                 Expression |
                      letrec_exp of (Variable list) *
                                    (Expression list) *
                                    Expression |
                      oper of Operator * Expression * Expression

So, now you have your "type" which is nothing else than a glorified
S-expr.  This is essentially my personal experience with *ML programs.

Yes.  I do believe that type inferencing does buy you a lot.  I just
do not think it buys you enough to make you switch.

After all

(defun foo (x) (+ x 3))
(defun baz () (car (foo 3)))

When compiling with CMUCL gives me the following

* (compile 'foo)
FOO
NIL
NIL

* (compile 'baz)
In: LAMBDA NIL
  (FOO 3)
Warning: Result is a NUMBER, not a (VALUES &OPTIONAL LIST &REST T).

Compilation unit finished.
  1 warning

BAZ
T
T

You may not consider this sufficient, but it is already a lot.

        ...

You insistence on "at the type level" you "prefer to return an option"
(it'd be nice to explain what this actually means) is just a fancy way
to say: my function will return a second value of NIL if the item is
not in the map.  E.g. this is what GETHASH does.  Somehow, I will have
to deal with the case,  but this is simply part of the "contract" the
function writer is asking me to respect.  There is nothing magical
about "types" in this context (unless I am grossly misunderstanding
something).

I.e. defining something like

datatype 'a result = item of 'a | not_found

fun find x [] = not_found
  | find x (first::rest) = if x = first then item(first) else find x rest

and then writing code that does not handle the `not_found' type
constant is just the same as writing code that does not handle the
NIL.

fun foo item(x) = x + 4

is definable (AFAIK) and all you will get is a warning about a
possible match exception.  Granted, it is better than doing

(defun find* (x list) ....)

(defun foo (x) (+ x 4))

(foo (find* 3 '(1 2 44)))

But the bottom line is that you will still get a runtime error if you
wrote

foo (find 3 [1, 2, 44])

And, at the end of the day, by moving to *ML, I have lost code and
data equivalency, a powerful macro system and multimethods.  This is
why I stick to CL, hoping that the compilers will improve their type
inferencing capabilites.

Cheers