1. Куча / Говнокод #27427

    +2

    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, 14 Мая 2021

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

    • SEO: неявные преобразования и до Coq добрались, причём пиздец неочевидные.
      Ответить
      • Это не неявные преобразования (которые там тоже есть, см. Coercion), емнип, просто if так устроен, что жрёт любой индуктивный тип с двумя конструкторами без аргументов.
        Ответить
        • Ага, причём верхний из них всегда труъ. Какой костыль )))
          Ответить
          • Так повелось, что в любой функциональщине if болтается как бедный родственник.
            Ответить
        • З.Ы. Просто не хотели костылить бул как особый тип? Поэтому then это верхняя ветка, а else нижняя?
          Ответить
          • > Просто не хотели костылить бул как особый тип?
            Как я говорил выше, в функциональщине синтаксис `if then else' любовью не пользуется, ибо есть паттерн-нятчинг. Поэтому и делают его на отъебись.

            > Поэтому then это верхняя ветка, а else нижняя?
            Да.
            Ответить
            • Зато если списки оформлять cons'ом вверх, то можно прям как в сишке или питоне проверять на пустоту if'ом!
              Ответить
            • А вот с числами в стандартной либе они обосрались. Можно было записать их нулём вниз, тогда работало бы как в сишке... А сейчас там if 0 уходит в ветку then.
              Ответить
        • Errata:

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

        Ого, и борманд того
        Ответить
    • > Proof.
      > reflexivity.

      Так вот оно какое, ИМПЕРАТИВНОЕ программирование!
      Ответить
    • Нахуй нужен "Coq"?
      Ответить
      • Чтобы доказывать всякую хуиту
        Ответить
        • Приведи реальный пример.
          Ответить
          • Theorem real_example:
              2 * 2 = 4.
            Proof.
              auto.
            Qed.
            Ответить
            • > реальный
              Ответить
              • Бекенд сишного конпелятора.
                Ответить
                • ты доказал корректность сишного компилятора через кок? Теперь он TCB, и можно для чернобыля и боинга писать софт?
                  Ответить
                  • Я не настолько девочка-волшебница, я только учусь. Это другие чуваки доказали.
                    Ответить
                    • Я просто вообще не в теме: у какого компилятора он доказан кроме CompCert (или как там сам проект называлсЯ)?
                      Ответить
                  • > чернобыля

                    Кстати, а почему в чернобыле новый реактор не строят? Хуже ведь не будет, даже если опять ёбнет.
                    Ответить
                    • В смысле снять саркофаг и построить новый?
                      Ответить
                      • Рядом.
                        Ответить
                        • Я не знаю какой там фон, насколько там хорошо жить, да и стрёмно наверное людей там рядом держать: испортят саркофаг еще
                          Ответить
                          • ващет люди там до сих пор есть, следят за ситуацией и проводят какие-то исследования

                            а станция работала как станция до конца 2000-го года
                            Ответить
                            • Автор одного известного в узких кругах юзерскрипта для вакабы некоторое время там работал, кстати. Его канальчик:
                              https://www.youtube.com/channel/UCpyhhhcrqGD2g74t-IYDuPA
                              Ответить
                              • канал слегка наполнен баянами для буржуйских туристов
                                Ответить
                          • > стрёмно наверное людей там рядом держать: испортят саркофаг еще

                            Супер Сус регулярно туда катается, пока ничего ещё не испортил.
                            Ответить
                    • Какой багор )))
                      Ответить
                    • зачем новый? там и так несколько блоков вполне себе работали после аварии
                      Ответить
                    • Туберкулезных я посылал бы на фронт, это им пойдет на пользу, да и, кроме того, — лучше терять убитыми больных, чем здоровых.
                      Ответить
                      • а ковидных?
                        Ответить
                      • Но биологическое оружие вроде запрещено...
                        Ответить
                        • Швейк воевал в первую мировую, тогда ещё не было душнил из ООН с их глубокой озабоченностью.
                          Ответить
                      • Проблема вагонетки?
                        Ответить
                      • Гашек всё таки охуенный чувак! Сто лет прошло, а как всё актуально до сих пор!
                        Ответить
                    • > Хуже ведь не будет, даже если опять ёбнет.

                      - конечно, ведь Новохуйск далеко, чего переживать
                      Ответить
                    • у них дизайн - жуткое говно, потому и ёбнул стоило только выйти за праздничным дефицитом
                      а купить стоит дохуя денег
                      да и собственно уран тоже надо откуда-то брать
                      в общем сложно, а на фоне тухлой репутации почти невозможно, поэтому идиоты немцы позакрывали всё чтобы жечь уголь
                      Ответить
                    • https://vk.com/wall-89379348_201620

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

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

                      Недавно ученые уже фиксировали растущие уровни нейтронов на ЧАЭС, но риска утечки пока нет, так как ситуация развивается очень медленно. Но если процесс не остановить, то возникает опасность увеличения тепловыделения. В свою очередь, оно может постепенно расплавить окружающий материал, что влечет за собой опасность проникновения в окружающую среду радиоактивных элементов.
                      Ответить
                  • А корректность софта кто докажет?
                    Ответить
                • Реальный, умещающийся в 40 строк.
                  Ответить
    • пиздец Бьёрне старый((
      https://twitter.com/KathrinPetrova/status/1237430865329819648
      Ответить
      • даже подписать не поленились
        а розетки присобачили криво
        https://pbs.twimg.com/media/ESw8tKCWoAEgewe?format=jpg&name=large
        котлин, хули
        Ответить

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