how 'safe' exactly does writing in a language like this really force you to be?
exactly as safe as the type system is. this paper didn't provide any formal proofs or statements of properties, so i really don't know what they mean. it seems like they were mostly talking about memory safety. proving things about concurrent code is still a Hard Problem as far as i'm aware.
will the innermost guts (context switcher, etc) still have to be written in asm, or does the language provide facilities for it?
they also, frustratingly, didn't talk about much of their implementation, other than the blurb i posted. but some of it is certainly in c, and i would assume the context switcher is in asm. maybe typed assembly? but at any rate, the kernel they provide is a trusted code base. they just want to keep that part small.
![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
no subject
Date: 2010-02-16 05:26 am (UTC)From:exactly as safe as the type system is. this paper didn't provide any formal proofs or statements of properties, so i really don't know what they mean. it seems like they were mostly talking about memory safety. proving things about concurrent code is still a Hard Problem as far as i'm aware.
will the innermost guts (context switcher, etc) still have to be written in asm, or does the language provide facilities for it?
they also, frustratingly, didn't talk about much of their implementation, other than the blurb i posted. but some of it is certainly in c, and i would assume the context switcher is in asm. maybe typed assembly? but at any rate, the kernel they provide is a trusted code base. they just want to keep that part small.