Warp wrote:
>   If you are doing a simple linear traversal, maybe, but if it's any more
> complicated than that...

Hmmm... Apparently there are mechanisms in place (which I don't really 
understand) that let you interactively prove to the compiler that some 
sequence of operations is safe, and then that gets recorded and the 
compiler can take advantage of it.  I.e., if you can prove that you 
never go out of bounds, even if the proof is "non-obvious" to the 
machine, then the compiler will omit the run-time checks.  Awesome.  :-)

Personally, I can't imagine how you go about doing such a thing, except 
maybe adding stuff to the code describing what/why you think it's true 
and running it thru the compiler again, which doesn't seem like 
"interactive" to me. But I'm not finding anything on line that isn't 
either "it's really cool" or "here's 40 pages of mathematics describing 
how it works."


Also, I imagine you could put in appropriate assertions, such that if 
you say (for example)

void flog(int[] myints, int startinx) {
   assert myints.length > 500;
   assert startinx > 100 && startinx < 400;
   for (int i = startinx - 50; i < startinx + 50; i++)
      myints[i] = myints[i+10];
}

then the compiler could track the possible ranges of values, and you'd 
get runtime checks at the entry to the function but not inside the loop, 
as an example.

But yeah, figuring out which next bit of object to bounce a ray off of 
is obviously going to take some run-time checks.

But honestly, I've never seen code where which element gets accessed 
next is obvious to a programmer but not to the compiler. I've never seen 
code where you could prove to a person's satisfaction that it was 
correctly accessing the array but couldn't prove it in a formal way 
given what's in the code itself, assuming you have all the code in front 
of you, of course.

Do you have any examples of that? I'm sure there must be some out there, 
but I don't do that sort of programming, I think. I think the closest 
I've gotten is knowing that the program that generated the file put 
things in it such that the program reading the file doesn't have to 
check. (E.g., the writer of the file never puts more than 80 chars per 
line, so the reader doesn't have to check, and that's because I wrote 
them both myself.)

-- 
Darren New / San Diego, CA, USA (PST)

Post a reply to this message