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

  • Бажок в Bluetooth PAN

    Нашёл тут два бажка в венде.. 1. Запускаете таск менеджер 2. Включаете в iOS hotspot (на ведроиде вроде называется Bluetooth Tethering) 3.…

  • Тайп-фу в TS

    У нас тут есть сторонний HTTP-сервис, возвращающий либо { success: true } либо { error: 42, description: "because" }. Ну и по openapi.yaml генерится…

  • Винда и 4гб

    Тут или крестик или трусы. Если у вас винда - то должно быть 6+ рамы. На 4-х WebStorm неюзабельный. С другой стороны, в 2021 4 гб на разрабской…

  • 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

  • Бажок в Bluetooth PAN

    Нашёл тут два бажка в венде.. 1. Запускаете таск менеджер 2. Включаете в iOS hotspot (на ведроиде вроде называется Bluetooth Tethering) 3.…

  • Тайп-фу в TS

    У нас тут есть сторонний HTTP-сервис, возвращающий либо { success: true } либо { error: 42, description: "because" }. Ну и по openapi.yaml генерится…

  • Винда и 4гб

    Тут или крестик или трусы. Если у вас винда - то должно быть 6+ рамы. На 4-х WebStorm неюзабельный. С другой стороны, в 2021 4 гб на разрабской…