Chris Hawblitzel and Juan Chen: Introduction to Typed Assembly Language (TAL)

Play Chris Hawblitzel and Juan Chen: Introduction to Typed Assembly Language (TAL)

The Discussion

  • User profile image
    Justin Bailey

    Great video! Juan Chen has done some really impressive work. In particular, she formalized a big chunk of the Sparc instruction set. Yes, typed machine language Smiley

    Greg Morrisett's papers are worth reading. I found "TALx86: A Realistic Typed Assembly Language" to be the most accessible (

    Atsushi Ohori wrote a paper that treats typed machine languages as proof systems. Very abstract but impressive too: "A Proof Theory for Machine Code" (

    Unfortunately none of the research compilers or languages (including Cyclone) evolved into something 'real'. Maybe Microsoft will release "Verified C#" with Visual Studio 2011??? Smiley

    Thanks for putting these two on, really cool to see!

  • User profile image

    Typed ASM should stay a research exercise.... Charles you usually over-hype this typed ASM for maybe for how cool it sounds. I don't think TAL is really a useful or productive mechanism in most ways/shapes/forms for the sum of these parts don't make a greater whole.  And I usually love cutting-edge research projects which try something new, but verification should stay up in a higher level.

    It would make more sense of have Intel and AMD make type-system's with API's and CPU flags which can allow the CPU itself to "type-check" the machine code jammed down it's pipeline. But for ASM source code to have that sort of overhead in the general case is complete overkill...  I think It's easier to have comments left in the ASM source and just as good to have signed and checksummed binaries which are verified by vendors and enthusiasts like me. Malicious coders will fake type safety just as easily if required since security can always be broken, I'd argue that it's even more fragile down there since there's less layers and encapsulation to prevent incorrect code from trying to run when it does happen.

    The ONLY way that a typed ASM may be used I can think of is to reverse engineer binaries into whatever source code language you want as long as it is strongly typed.  Instead of just reverse engineering the binary into the original source code language for it to have actual meaning.

    Verve would undoubtedly benefit from this sort of work and for projects similar to Verve, but its application is way too small for this type of research to benefit anything but a statically verifiable kernel and theorem provers.

    Continue the good work but I hope Hawblitzel moves on to even more interesting and beneficial research areas instead of focusing on this particular domain too long unless this exact domain is his passion, in this case hell, take my words as a grain of salt, I'll never suggest a true researcher to research anything but what he/she loves. Smiley

  • User profile image

    @HeavensRevenge: Fine. Smiley In my defense, however, it's not really over-hyped geek marketing of TAL... Rationally, I disagree with you regarding its usefulness. It's at least as useful as IL... Anyway, we do talk about it's usefulness outside the scope of academia.

    Did you watch this video (or listen to it)?  (Sorry about how loud my voice is - I need to move further behind the camera or just get lav mics and a new camera that supports them... Also, I purposely kept the conversation at a higher level, though not too high, since the more techincal audience can get more details from the related papers linked to in the description).

    TAL is as much about building better/more reliable/verifiable compilers as it is about building machine-verifiable software systems, beginning just above the machine (assembly is the lowest level of human-readable software abstraction) and ending up in the playful, cozy bubbles of user experience... Then, yes, there's the over-Charles-hyped uber coolness factor of downloading typed x86 from some service and executing it without remorse (well...)... Smiley

    Keep on pushing the envelope Chris and Juan. Yours is a bright future.

  • User profile image

    Juan Chen on Channel 9 finally! Cool stuff, thank you Charles. Smiley

  • User profile image

    @felix9: My hope is that she will reappear.

  • User profile image

    This is one of final check of compiler to make sure codes generated correctly. There were few bugs related to c# codes that compiler create a big hole when executed. This is a big safety check

  • User profile image

    Very good video, made ​​me feel excited again Smiley

    The first time I was teaching was Operating Systems, some years ago. Good times. I have heard some stuff about Microsoft research on experimental OS that uses a sort of C#, it's good know now what it is and how it works. My old friend, who teaches Compilers will be interested in this video.

    @Charles: More good people to the friends list to make videos! Thank Hawblitzel and Chen and for us.

  • User profile image

    TAL doesn't make sense to me.
    Both C# and MSIL are type safe so TAL isn't needed.
    So the code is checked 2 times.

    To me TAL is just a waste of time, money and cpu cycles.

    If TAL is usable on C++ (for real programmer) then the compiler team can use this as a internal verification thingy.
    (visual studio compiler do have many bugs, too many!!)

    other then that plain waste.
    Just another vista-idea i say. (Slow, waste of time, hardware hungry, etc ,etc... )

  • User profile image

    Another layer of indirection to slow things...

Add Your 2 Cents