[hcs]

Never heard of it, link?

[zeptomu]

"Applied Type System" - a language built for correct low-level programming inspired by functional programming and theorem proving.

http://lmgtfy.com/?q=ats+language

If I remember correctly there were plans to implement GNU Hurd (the Half-Life 3 of kernels) in ATS, but that probably went nowhere. But there is a small osdev community messing with kernels and ATS.