This code is there not for performance

Posted Feb 12, 2008 14:38 UTC (Tue) by nix (subscriber, #2304)
In reply to: This code is there not for performance by ms
Parent article: vmsplice(): the making of a local root exploit

That's nice in theory, but I'm not sure it's entirely practical to require the users to
provide a different pointer type for every possible VM range!

(Also, kernel/user boundaries are necessarily special places: typing across the boundary is a
matter of consensus as much as enforcement.)

This code is there not for performance

Posted Feb 12, 2008 14:49 UTC (Tue) by ms (subscriber, #41272) [Link] (6 responses)

Yeah, I don't disagree. It is a hard thing to do - you tend to get into messes with
dependently typed languages and so forth - one could easily argue that they're not quite ready
for writing kernels in!

Typically, you first implement maths in the type system, then you can implement a basic "is
smaller than" so then you could effectively arbitrarily refine the int range to be "the value
must be an int and must also be smaller than x". That kinda thing. Of course, as soon as you
hit "the value must be a function which will terminate", you're in trouble...!

This code is there not for performance

Posted Feb 12, 2008 15:05 UTC (Tue) by nix (subscriber, #2304) [Link] (5 responses)

There are a good few languages (Cayenne and Qi spring to mind) with type systems that are so
powerful that they themselves trip the halting problem: compilation is no longer guaranteed to
terminate. :)

I suppose a simple ranged length type (length must be >0) would have sufficed here: you
wouldn't need separate types for every possible valid pointer range.

Halting problem ? Ha!

Posted Feb 12, 2008 20:17 UTC (Tue) by khim (subscriber, #9252) [Link] (4 responses)

C++ has them beat: it's type system is not just trigger halting problem, it's turing-complete!

Halting problem ? Ha!

Posted Feb 12, 2008 21:00 UTC (Tue) by nix (subscriber, #2304) [Link]

C++'s template expander is modelled on ML's pattern matching. Cayenne and 
Qi are both perhaps two generations beyond that (both type systems being 
more powerful than Haskell's) in different directions: personally I prefer 
Qi's, but part of that is probably because it's possible to bootstrap the 
Qi implementation without being an ultra-guru).

Of course, C++ compilers often *appear* to not halt when compiling 
anyway ;}

Halting problem ? Ha!

Posted Feb 14, 2008 22:01 UTC (Thu) by lysse (guest, #3190) [Link] (2 responses)

I don't know if you're joking about C++, but one of the notable things about Qi is that its
type system *is* Turing-complete, by intent and proof (someone implemented SK combinators in
it).

Halting problem ? Ha!

Posted Feb 15, 2008 0:06 UTC (Fri) by ms (subscriber, #41272) [Link] (1 responses)

No, nix wasn't joking. If you use C++ templates and limit yourself to numbers then it really
is turing complete. Haskell, with the right flags (undecidable instances and overlapping
instances) is also Turing complete. Cayenne is deliberately so and many people are now really
thinking that it's just better to permit Turing completeness and let the programmer take
responsibility.

The alternative is more like what Epigram is looking at (amongst others) where you limit
recursion to on the structure of terms and prevent infinite structures. That way, you can
still guarantee termination. I fear we may now be some way from the original issue though ;)

Halting problem ? Ha!

Posted Feb 15, 2008 21:48 UTC (Fri) by nix (subscriber, #2304) [Link]

I used the wrong terms, really. What Haskell, Cayenne and Qi provide over 
C++ is (radically) greater *expressiveness*. The syntax of Qi type 
definitions is especially strange, but it's a hell of a lot saner than 
trying to define anything complicated using C++ templates.