BitC, Johns Hopkins Üniversitesi'ndeki araştırmacılar ve The EROS Group, LLC tarafından Coyotos projesinin bir parçası olarak geliştirilen, kısmen tasarlanmış ve uygulanmış bir sistem programlama dili idi. Resmi program doğrulamasını desteklemeyi amaçladı. BitC'nin birincil tasarımcısı, 2012'de temel tasarım hatalarına sahip olduğunu iddia ederek dil üzerinde çalışmayı bıraktı. Dilin iki ana hedefi vardır: Modern programlama dillerinin gelişmelerini birleştirmek; Soyutlama, ses ve eksiksiz türeme, let-polimorfizm ve matematiksel olarak kurgulanmış semantik - sistem programlamasının gereklilikleri ile ses türü sistemler; Birinci sınıf devlet muamelesi, reçeteli alt düzey sunum için destek, açıkça kutu içine girilmemiş türler ve C ile karşılaştırılabilir performans. Çekirdek / mikro çekirdek gibi düşük seviyeli sistem programlarının resmi program doğrulamasını desteklemek. BitC dilinin hedefleri, 2004'te NICTA OS Doğrulama Çalıştayı'nda sunulan Doğrulanmış, Ge