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

Цели

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

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

Достижения

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

Состояние

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

См. также

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

Примечания

Ссылки

• (неопр.) .