kouzdra (kouzdra) wrote,
kouzdra
kouzdra

Categories:

Не прошло и 15 лет, как в голове сложилась картинка

- Я вообще кажется понял чем на самом деле занимается INRIA (или по крайней мере значительная ее часть) - вот этим и занимается - технологиями для разработки safety critical systems - тут практически куда не плюнь - рано или поздно вылезают уши INRIA.

SCADE - из INRIA уши растут, SPARK на ихнем движке работает, язычок F* на котором я примеры как раз приводил - сопродукция MS Research и INRIA (щас ушел полностью под INRIA), И кстати казавшийся мне странным их выбор проектов на деле совершенно логичен и даже довольно прикладного свойства.

Совершенно не удивлюсь если окажется что спонсируют все это EADS и Areva с лягушачьим министерством обороны на паях. Точнее довольно сильно удивлюсь если это не так.

И кстати особенности эволюции OCaml ясны - он под конкретные задачи на сам деле развивается

PS: Coq кстати тоже давно уже не только абстрактная формализация математики, а один из самых мощных движков под это дело (в принципе тот же why3 может и его использовать) - просто как я понимаю для end-user-овского продукта сложноват в использовании

Xavier Leroy кстати занимается щас compcert - полностью верифицированным компилятором С (сейчас утверждается, что на 90% примерно) - тоже когда первый раз узнал очень удивился - а сейчас все на свои места тоже стало
Subscribe

  • "Трагедия курьера"

    Что забавно - попытки партии и ментов усиливать контроль за всем на практике дают противоположный результат - паспорта у меня в данный момент нет,…

  • Из комментов

    Впрочем у истории с чёрными кораблями были две забавные концовки — одна в Порт-Артуре, другая — в Жемчужной гавани

  • Во всяком культивировании

    всяких покрытых богоматерей, дней оун-упа и прочих мининых-невских-пожарских и тп меня раздражают не поводы (на них мне действительно насрать) а…

  • Post a new comment

    Error

    default userpic

    Your reply will be screened

    Your IP address will be recorded 

    When you submit the form an invisible reCAPTCHA check will be performed.
    You must follow the Privacy Policy and Google Terms of use.
  • 4 comments