Advocacy (Was: Who here actually uses D?)

[bearophile]

> (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