[Из песочницы] F* – новый язык с зависимыми типами для .Net
Введение F* — это новый язык с зависимыми типами, разработанный в недрах Microsoft Research для построения доказательств свойств программ. F* компилируется в байткод .Net и прозрачно интегрируется с другими языками, включая F#, на основе которого он и построен. Вы можете попробовать F* в браузере или скачать альфа-версию компилятора и сопутствующих примеров тут. Формализация F* в системе Coq доступна для всех желающих.Читать дальше →
