On Wed, Jul 15, 2015 at 2:26 AM, Keean Schupke <[email protected]> wrote:
> If you can prove the runtime safe, then its a safe language right? When I am
> talking about a safe language, I am including proving things.
>
> For example 'C' with a different type system, where safety can be proved in
> the type system would be a safe language.
>
> Bytecode interpreted languages are only a subset of safe languages, and one
> specific implementation technique. I would rather compilevto native, no
> runtime, and using proofs. You need to combine the proof requirement into
> the compiler, so it will not compile unsafe code.

Ah! Yes, that sounds great. But yeah: that's pretty darn hard.
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev

Reply via email to