BitC — язык системного программирования, разработанный исследователями Университета Джонса Хопкинса и The EROS Group как часть проекта Coyotos^[англ.]. Типобезопасен, ориентирован на разработку надёжных (верифицируемых) встраиваемых систем, драйверов и других задач системного программирования.

Язык создавался с целью решить две основные задачи:

1. Объединить достижения современных языков программирования при сохранении производительности языка Си.
2. Упростить верификацию низкоуровневых программ, таких как ядро/микроядро операционной системы.

На данный момент на BitC возможно реализовать MPEG-декодер или алгоритм криптографического хеширования SHA-1, которые будут иметь доказанную безопасность, и при этом соперничать в быстродействии с реализацией на Си. Этого невозможно добиться на Standard ML, OCaml или Haskell.^{[2][аффилированный источник?]}

В апреле 2009 года главный разработчик, Джонатан Шапиро^[3], объявил, что принял предложение Microsoft по работе над операционной системой Midori и в августе прекратит работу над языком программирования^[4]. В марте 2010 года он объявил, что покидает Microsoft и продолжит работу над BitC^[5]. Однако, в марте 2012 он сообщил, что окончательно прекращает разработку, так как язык имеет фундаментальные ошибки в дизайне и в текущем виде работать не будет^[6]. 26 февраля 2015 года на официальном сайте было объявлено о работе над версией 0.2 спецификации языка^[7].

• Формальная верификация
• Cyclone

• Домашная страница проекта
• Спецификация языка
• BitC-dev архив рассылки
• Страница проекта Coyotos
• Домашняя страница Джонатана Шапиро
• ChampReview: The BitC Programming Language  (неопр.).