Расскажите, пожалуйста, про Why3 (ну, в смысле, хотели бы вы его использовать в вашем идеальном проекте или нет)

Formalising the semantics of programming language is most of the time done using interactive proof assistants like Coq or Isabelle. Yet, formalising semantics and proving complex properties, with automatic provers only, was already shown possible by Clochard et. al, who also use the Why3 environment.

Здравствуйте, Эйнсток Файр, Вы писали:

ЭФ>Расскажите, пожалуйста, про Why3 (ну, в смысле, хотели бы вы его использовать в вашем идеальном проекте или нет)
ЭФ>

Formalising the semantics of programming language is most of the time done using interactive proof assistants like Coq or Isabelle. Yet, formalising semantics and proving complex properties, with automatic provers only, was already shown possible by Clochard et. al, who also use the Why3 environment.

Да, хотел бы. Если бы мне дали денег на переписывание линукса с Си на что-то более разумное.

В Касперском вроде бы этим уже занимаются, правда не переписывают, а пишут с нуля.

Здравствуйте, Слава, Вы писали:

С>В Касперском вроде бы этим уже занимаются, правда не переписывают, а пишут с нуля.

на что в Касперском переписывают ?

Я бы дафни хотел, но он какой-то недопиленый (ну что это такое со строками, в самом деле) да и кому оно надо