> (but they too use twenty modules written in a kind of typed and proved > assembly).
This is from a conference by Linus and friends: http://www.linuxjournal.com/article/7272 >I am a huge believer in static typechecking that doesn't add any runtime >overhead. So you basically get perfect performance, assuming your compilers >are perfect--whatever--with reasonably good safety. The problem is that being >the kernel has to do a lot of things that break typechecking. Which you see >more in the kernel than in a lot of other programs. You end up having a lot of >inline assembly which is obviously completely opaque.< The interesting experimental Verve operating system contains some typed assembly too, so I've taken a better look at this idea. This is a site about typed assembly: http://www.cs.cornell.edu/talc/ Some papers: http://www.cs.cornell.edu/talc/papers.html Typed Assembly Language (TAL) is different from High Level Assembly (HLA, http://webster.cs.ucr.edu/AsmTools/HLA/ ) because TAL is mostly a way to add type annotations to normal assembly code. I have written some X86 assembly code and some other kind of assembly code, and I have seen how much bug-prone it is. I know that compared to C the asm is so bug-prone also because there is no type system to catch bugs. So the idea of type annotations for asm code is interesting for me. So a D compiler may perform normal type tests of the inlined asm code that uses type annotations (in theory this doesn't even require to modify the D front-end, an external tool may be used to test the type annotations). As reference I use two papers: Dan Grossman, Greg Morrisett, "Scalable Certification for Typed Assembly Language": http://www.cs.cornell.edu/talc/papers/tal_scale.pdf Greg Morrisett et al., "TALx86: A Realistic Typed Assembly Language": http://www.cs.cornell.edu/talc/papers/talx86-wcsss.pdf Quotations: As in a conventional assembly language, the instructions and data are organized into labeled sequences. Unlike conventional assembly language, some labels are equipped with a type annotation. The type annotations on the labels of instruction sequences, called code types, specify a pre-condition that must be satisfied before control may be transferred to the label. The pre-condition specifies, among other things, the types of registers and stack slots.< For example, if the code type annotating a label L is {eax:int4, ebx:S(3), ecx: ^*[int4,int4]}, then control may be transferred to the address L only when the register eax contains a 4-byte integer, the register ebx contains the integer value 3, and the register ecx contains a pointer (^) to a record (*[...]) of two 4-byte integers. Bye, bearophile
