clueless newbie re: dependent types

[Raoul Duke]

http://blog.llvm.org/2011/05/what-every-c-programmer-should-know.html

how many of those things could be modeled by dependent types so that we'd still be able to get the optimizations? we'd statically know if we've dereferenced null, or if we've not 0'd out a memory allocation, etc.?

[Brandon Barker]

I'm pretty sure that all of these are handled in ATS2 by linear or dependent types, but there is one I'm not sure about.

It is possible I've gotten the categorizations wrong but this is my understanding:

dependent:

Signed integer overflow 

Dereferencing a NULL Pointer

linear:

Violating Type Rules (e.g. use castfn in ATS2 where appropriate, and use the correct views)

Use of an uninitialized variable

linear or dependent:

Dereferences of Wild Pointers and Out of Bounds Array Accesses 

other:

Oversized Shift Amount (I'm not sure about this one, but it seems that it is possible to do this safely, if not necessarily as efficiently as doing it unsafely. But I think dependent types could be used to do this safely, as you just define the shift amount as a size < 32).

Brandon Barker
brandon...@gmail.com

On Fri, Mar 14, 2014 at 4:37 PM, Raoul Duke <rao...@gmail.com> wrote:

http://blog.llvm.org/2011/05/what-every-c-programmer-should-know.html

how many of those things could be modeled by dependent types so that we'd still be able to get the optimizations? we'd statically know if we've dereferenced null, or if we've not 0'd out a memory allocation, etc.?

--
You received this message because you are subscribed to the Google Groups "ats-lang-users" group.
To unsubscribe from this group and stop receiving emails from it, send an email to ats-lang-user...@googlegroups.com.
To post to this group, send email to ats-lan...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/07233cfe-e517-4e3d-ae2a-07413023b033%40googlegroups.com.

[gmhwxi]

All these can certainly be modeled. The real point is whether someone is willing to
go through the trouble to make sure that 'undefined behavior' is not relied upon.