kouzdra (kouzdra) wrote,
kouzdra
kouzdra

This journal has been placed in memorial status. New entries cannot be posted to it.

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

  • "И все его оставили"

    Чего0то мне кажется, что на Украине жизнь скоро может начать иллюстрировать искусство: Когда случился тот неслыханный скандал, тот крик, и брань, и…

  • Технологии

    "... держать молоток либо какие-то новые технологии...", – считает Володин.

  • Попались обсуждения какого-то

    гопнического сериала про "слова пацанов", там в воспоминательных рассуждаловах всякие личные воспоминание про "с раёнов" - поражает театраьность и…

  • Post a new comment

    Error

    Comments allowed for friends only

    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded 

  • 4 comments