Hello again
Me:
What if I don't trust your kernel?
[..]
What's the downloadable object that can be machine-checked to satisfy
my paranoid insurance company?
Oleg:
I hope that you can forgive me if I reply by
quoting the above two paragraphs back to you, with the substitution
s/kernel/compiler/.
Hello!
Bjorn Lisper wrote:
> What is the relation to the sized types by Lars Pareto and John Hughes?
It is orthogonal and complementary, as the message in response to
Conor T. McBride indicated.
> What is the relation to classical range analyses for (e.g.) array index
> expressions, which have
Hello!
> What if I don't trust your kernel? The guarantees you require of
> your kernel are not statically checked. What guarantee do I have
> that the propositions which you identify are even the ones which
> are really needed to eliminate bounds checking? How does the
> machine replace ! by uns
Hello Oleg, hello all
I agree with you on this:
[EMAIL PROTECTED] wrote:
There is a view that in order to gain static assurances such as an
array index being always in range or tail being applied to a
non-empty list, we must give up on something significant: on data
structures such as arrays (to be
( A really interesting post on static elimination of array bounds checking
by Oleg...)
Some questions and suggestions:
What is the relation to the sized types by Lars Pareto and John Hughes?
What is the relation to classical range analyses for (e.g.) array index
expressions, which have been know
There is a view that in order to gain static assurances such as an
array index being always in range or tail being applied to a
non-empty list, we must give up on something significant: on data
structures such as arrays (to be replaced with nested tuples), on
general recursion, on annotation-free
