Andy Melnikov (nponeccop) wrote,
Andy Melnikov
nponeccop

Category:

Contracts first

Тут из альтернативной вселенной сообщают, что завтипы говно и не нужны.

Вместо этого берете язык с простыми типами и контрактами в стиле Eiffel https://www.eiffel.com/values/design-by-contract/introduction/ и скармливаете статик ассерты в http://why3.lri.fr/#users которая дальше их скармливает пруверам из списка http://why3.lri.fr/#provers

Оно и в кок конечно умеет скармливать, но пруверы для конечных теорий (типа SMT FixedSizeBitVectors) по понятным причинам и работают лучше, и точнее моделируют машинное представление.
Tags: fp, hn0, programming, до чего техника дошла
Subscribe

  • Cубботний Unicode WTF

    Я тут переехал локально, старый хозяин изъявил желание, чтобы я пиздовал нахуй. Ну и на новом месте почему-то нету покрытия GPON, так что старый…

  • Вышел CentOS 7 for i386

    Вы будете смеяться, но через 6 лет выпустили таки. https://lists.centos.org/pipermail/centos-announce/2020-November/035819.html…

  • 3des-cbc!

    Это я поотключал левые шифры, и повключал логи в опенссш. И вот что любители посканировать предлагают: Unable to negotiate with X.X.X.X port YYYYY:…

  • 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.
  • 11 comments

  • Cубботний Unicode WTF

    Я тут переехал локально, старый хозяин изъявил желание, чтобы я пиздовал нахуй. Ну и на новом месте почему-то нету покрытия GPON, так что старый…

  • Вышел CentOS 7 for i386

    Вы будете смеяться, но через 6 лет выпустили таки. https://lists.centos.org/pipermail/centos-announce/2020-November/035819.html…

  • 3des-cbc!

    Это я поотключал левые шифры, и повключал логи в опенссш. И вот что любители посканировать предлагают: Unable to negotiate with X.X.X.X port YYYYY:…