Куча говна / Говнокод #27427 Ссылка на оригинал

0

  1. 1
  2. 2
  3. 3
  4. 4
  5. 5
  6. 6
  7. 7
  8. 8
  9. 9
Inductive my_bool :=
| my_false
| my_true.

Theorem shit_happens:
  (if my_false then 42 else 100500) = 42.
Proof.
  reflexivity.
Qed.

Какая типизация )))

Запостил: bormand bormand, (Updated )

Комментарии (70) RSS

  • ava bormand # Ссылка на оригинал 0

    SEO: неявные преобразования и до Coq добрались, причём пиздец неочевидные.
    Ответить

    • ava CHayT # Ссылка на оригинал 0 ⇈

      Это не неявные преобразования (которые там тоже есть, см. Coercion), емнип, просто if так устроен, что жрёт любой индуктивный тип с двумя конструкторами без аргументов.
      Ответить

      • ava bormand # Ссылка на оригинал 0 ⇈

        Ага, причём верхний из них всегда труъ. Какой костыль )))
        Ответить

        • ava CHayT # Ссылка на оригинал 0 ⇈

          Так повелось, что в любой функциональщине if болтается как бедный родственник.
          Ответить

      • ava bormand # Ссылка на оригинал 0 ⇈

        З.Ы. Просто не хотели костылить бул как особый тип? Поэтому then это верхняя ветка, а else нижняя?
        Ответить

        • ava CHayT # Ссылка на оригинал 0 ⇈

          > Просто не хотели костылить бул как особый тип?
          Как я говорил выше, в функциональщине синтаксис `if then else' любовью не пользуется, ибо есть паттерн-нятчинг. Поэтому и делают его на отъебись.

          > Поэтому then это верхняя ветка, а else нижняя?
          Да.
          Ответить

          • ava bormand # Ссылка на оригинал 0 ⇈

            Зато если списки оформлять cons'ом вверх, то можно прям как в сишке или питоне проверять на пустоту if'ом!
            Ответить

          • ava bormand # Ссылка на оригинал 0 ⇈

            А вот с числами в стандартной либе они обосрались. Можно было записать их нулём вниз, тогда работало бы как в сишке... А сейчас там if 0 уходит в ветку then.
            Ответить

      • ava CHayT # Ссылка на оригинал 0 ⇈

        Errata:

        просто if так устроен, что жрёт любой индуктивный тип с двумя конструкторами без аргументов.
        Ответить

  • ava JloJle4Ka # Ссылка на оригинал 0

    > Proof.
    > reflexivity.

    Так вот оно какое, ИМПЕРАТИВНОЕ программирование!
    Ответить

              • ava MAKAKA # Ссылка на оригинал 0 ⇈

                ты доказал корректность сишного компилятора через кок? Теперь он TCB, и можно для чернобыля и боинга писать софт?
                Ответить

                • ava bormand # Ссылка на оригинал 0 ⇈

                  Я не настолько девочка-волшебница, я только учусь. Это другие чуваки доказали.
                  Ответить

                  • ava MAKAKA # Ссылка на оригинал 0 ⇈

                    Я просто вообще не в теме: у какого компилятора он доказан кроме CompCert (или как там сам проект называлсЯ)?
                    Ответить

                • ava bormand # Ссылка на оригинал 0 ⇈

                  > чернобыля

                  Кстати, а почему в чернобыле новый реактор не строят? Хуже ведь не будет, даже если опять ёбнет.
                  Ответить

                      • ava MAKAKA # Ссылка на оригинал 0 ⇈

                        Я не знаю какой там фон, насколько там хорошо жить, да и стрёмно наверное людей там рядом держать: испортят саркофаг еще
                        Ответить

                  • ava Desktop # Ссылка на оригинал 0 ⇈

                    зачем новый? там и так несколько блоков вполне себе работали после аварии
                    Ответить

                  • ava CHayT # Ссылка на оригинал 0 ⇈

                    Туберкулезных я посылал бы на фронт, это им пойдет на пользу, да и, кроме того, — лучше терять убитыми больных, чем здоровых.
                    Ответить

                  • ava Desktop # Ссылка на оригинал 0 ⇈

                    > Хуже ведь не будет, даже если опять ёбнет.

                    - конечно, ведь Новохуйск далеко, чего переживать
                    Ответить

                  • ava gologub # Ссылка на оригинал 0 ⇈

                    у них дизайн - жуткое говно, потому и ёбнул стоило только выйти за праздничным дефицитом
                    а купить стоит дохуя денег
                    да и собственно уран тоже надо откуда-то брать
                    в общем сложно, а на фоне тухлой репутации почти невозможно, поэтому идиоты немцы позакрывали всё чтобы жечь уголь
                    Ответить

                  • ava guest # 0 ⇈

                    https://vk.com/wall-89379348_201620

                    Опасения по поводу саркофага Чернобыльской АЭС

                    В ядерном топливе, которое похоронено вместе с разрушенным четвертым энергоблоком Чернобыльской атомной электростанции, усилились реакции деления. Ученые обеспокоены возможностью повторения катастрофы. Растущую активность нейтронов засекли специальные датчики, установленные на ЧАЭС.

                    Недавно ученые уже фиксировали растущие уровни нейтронов на ЧАЭС, но риска утечки пока нет, так как ситуация развивается очень медленно. Но если процесс не остановить, то возникает опасность увеличения тепловыделения. В свою очередь, оно может постепенно расплавить окружающий материал, что влечет за собой опасность проникновения в окружающую среду радиоактивных элементов.
                    Ответить

                • ava guest # 0 ⇈

                  А корректность софта кто докажет?
                  Ответить

              • ava guest # 0 ⇈

                Реальный, умещающийся в 40 строк.
                Ответить

Добавить комментарий

Помни, guest, за тобой могут следить!

    А не использовать ли нам bbcode?

    ↑
    8
    ↓