OberonCore
https://forum.oberoncore.ru/

The BitC Programming Language
https://forum.oberoncore.ru/viewtopic.php?f=72&t=2457		 Страница 1 из 1
Автор:  Geniepro [ Пятница, 19 Март, 2010 09:49 ]
Заголовок сообщения:  The BitC Programming Language
Лиспоподобный язык для системных задач, был разработан для написания на нём верифицированных ядер операционных систем.

Цитата:
BitC is a new systems programming language. It seeks to combine the flexibility, safety, and richness of Standard ML or Haskell with the low-level expressiveness of C.

Цитата:
As a litmus test, it is possible to write a MPEG decoder or SHA-1 hash algorithm in BitC that is fully safe, but performs competatively with the C implementation. Today, that can't be done in SML, O'Caml, or Haskell.


Автор языка -- Jonathan Shapiro, год назад уходя из своего универа в Майкрософт, собирался забросить BitC, но сейчас собрался вернуться и с новыми силами взяться за этот язык.
Автор:  Rifat [ Пятница, 19 Март, 2010 12:37 ]
Заголовок сообщения:  Re: The BitC Programming Language
Geniepro писал(а):
Лиспоподобный язык для системных задач, был разработан для написания на нём верифицированных ядер операционных систем.

Хотелось бы узнать как делается верификация для функциональных языков. Читал, что верификация для функциональных языков делается достаточно просто, но сам метод верификации не видел. Может кто-нибудь просто и доступно объяснить как оно делается или же дать ссылку, где хорошо объяснено?
Автор:  Geniepro [ Пятница, 19 Март, 2010 14:00 ]
Заголовок сообщения:  Re: The BitC Programming Language
Начинать, наверное, надо с изучения литературы по таким языкам, как Coq, Agda2, тот же BitC. К сожалению, на русском такую доходчивую информацию я не видел.
"The Algebra of Programming" вроде как фундаментальна в этом плане, правда, говорят, трудное чтиво...

Вложения:
Комментарий к файлу: The Algebra of Programming (Prentice-Hall International Series in Computer Science)
Richard Bird, Oege de Moor

Describes an algebraic approach to programming that permits the calculation of programs. Introduces the fundamentals of algebra for programming. Presents paradigms and strategies of program construction that form the core of Algorithm Design. Discusses functions and categories; applications; relations and allegories; datatypes; recursive programs, optimization issues, thinning algorithms, dynamic programming and greedy algorithms. Appropriate for all programmers.
aop.djvu [1.71 МБ]
Скачиваний: 330
Автор:  Илья Ермаков [ Пятница, 19 Март, 2010 14:02 ]
Заголовок сообщения:  Re: The BitC Programming Language
Суть любой верификации в том, что описание в одной формальной модели-нотации представляется параллельно в другой, с доказательством эквивалентности. Например, программа и вывод в предикатах; или формальная спецификация - и построенная по ней программа на ФЯ.

Суть не в самой формалистике (в ней всегда "не суть"), а в том, что совершить одну и ту же ошибку и в одной форме, и в другой - очень маловероятно.
Автор:  Rifat [ Пятница, 19 Март, 2010 14:40 ]
Заголовок сообщения:  Re: The BitC Programming Language
Geniepro писал(а):
Начинать, наверное, надо с изучения литературы по таким языкам, как Coq, Agda2, тот же BitC. К сожалению, на русском такую доходчивую информацию я не видел.
"The Algebra of Programming" вроде как фундаментальна в этом плане, правда, говорят, трудное чтиво...

Спасибо за книжку. Хотелось бы, конечно, более доходчивого объяснения. Например, про доказательство программ на императивных языках, можно сказать, что программу надо строить параллельно с доказательством и нужно рассматривать инварианты, предусловия и постусловия.
Вот примерно так хотелось бы получить в нескольких словах общую идею верификации программ на функциональных языках.
Автор:  Geniepro [ Пятница, 19 Март, 2010 15:10 ]
Заголовок сообщения:  Re: The BitC Programming Language
Rifat писал(а):
Вот примерно так хотелось бы получить в нескольких словах общую идею верификации программ на функциональных языках.

Не, ну если в нескольких словах, то примерно так же и в ФП...
Автор:  Rifat [ Пятница, 19 Март, 2010 15:24 ]
Заголовок сообщения:  Re: The BitC Programming Language
Тогда может лучше указать различия. Инварианта цикла скорее всего не будет, так как в функциональных языках обычно не бывает циклов. Как обходятся без инварианта цикла? Что используют вместо него?
Автор:  Geniepro [ Пятница, 19 Март, 2010 15:51 ]
Заголовок сообщения:  Re: The BitC Programming Language
Rifat писал(а):
Тогда может лучше указать различия. Инварианта цикла скорее всего не будет, так как в функциональных языках обычно не бывает циклов. Как обходятся без инварианта цикла? Что используют вместо него?

Будет не инвариант цикла, а индуктивное доказательство корректности рекурсивной функции.
Автор:  Peter Almazov [ Пятница, 19 Март, 2010 16:57 ]
Заголовок сообщения:  Re: The BitC Programming Language
Geniepro писал(а):
Будет не инвариант цикла, а индуктивное доказательство корректности рекурсивной функции.
А Вы его хоть раз делали? Только честно :)
Автор:  Geniepro [ Понедельник, 22 Март, 2010 12:51 ]
Заголовок сообщения:  Re: The BitC Programming Language
Peter Almazov писал(а):
Geniepro писал(а):
Будет не инвариант цикла, а индуктивное доказательство корректности рекурсивной функции.
А Вы его хоть раз делали? Только честно :)

Только для простеньких, в образовательных целях.
Ну так инварианты циклов в сях и паскалях я вообще никогда не делал -- как-то так всю жизнь без них обходился.
Все циклы и рекурсии, которые я делаю, просты и потому очевидно правильны. А если и неправильны, то тут же исправляются. Ошибки обычно в других местах.

В ФЯ рекурсий не так уж и много -- композиция функций позволяет обходиться без рекурсий. map/fold/filter/zip -- и не надо никаких рекурсий...
Страница 1 из 1 Часовой пояс: UTC + 3 часа
Powered by phpBB® Forum Software © phpBB Group
https://www.phpbb.com/