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

    • ava bormand 14.05.2021 17:06 # 0

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

      • ava CHayT 14.05.2021 17:08 # +2

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

        • ava bormand 14.05.2021 17:09 # +1

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

          • ava CHayT 14.05.2021 17:18 # +1

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

        • ava bormand 14.05.2021 17:18 # +1

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

          • ava CHayT 14.05.2021 17:23 # +1

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

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

            • ava bormand 14.05.2021 17:24 # +1

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

            • ava bormand 14.05.2021 17:27 # 0

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

        • ava CHayT 14.05.2021 17:28 # +1

          Errata:

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

      • ava DypHuu_niBEHb 14.05.2021 18:38 # +3

        > Coq

        Ого, и борманд того
        Ответить

    • ava JloJle4Ka 14.05.2021 17:08 # +1

      > Proof.
      > reflexivity.

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

    • ava MATEMATuK_u3_PAIIIKu 14.05.2021 22:25 # 0

      Нахуй нужен "Coq"?
      Ответить

      • ava MAKAKA 14.05.2021 22:26 # 0

        Чтобы доказывать всякую хуиту
        Ответить

        • ava MATEMATuK_u3_PAIIIKu 14.05.2021 22:26 # 0

          Приведи реальный пример.
          Ответить

          • ava bormand 14.05.2021 22:38 # 0 

            Theorem real_example:
  2 * 2 = 4.
Proof.
  auto.
Qed.
            Ответить

            • ava guest6 14.05.2021 23:01 # 0

              > реальный
              Ответить

              • ava bormand 14.05.2021 23:06 # 0

                Бекенд сишного конпелятора.
                Ответить

                • ava MAKAKA 14.05.2021 23:07 # 0

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

                  • ava bormand 14.05.2021 23:08 # 0

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

                    • ava MAKAKA 14.05.2021 23:10 # 0

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

                  • ava bormand 14.05.2021 23:10 # +2

                    > чернобыля

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

                    • ava MAKAKA 14.05.2021 23:12 # 0

                      В смысле снять саркофаг и построить новый?
                      Ответить

                      • ava bormand 14.05.2021 23:12 # 0

                        Рядом.
                        Ответить

                        • ava MAKAKA 14.05.2021 23:13 # 0

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

                          • ava Desktop 14.05.2021 23:33 # +3

                            ващет люди там до сих пор есть, следят за ситуацией и проводят какие-то исследования

                            а станция работала как станция до конца 2000-го года
                            Ответить

                            • ava CHayT 14.05.2021 23:49 # 0

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

                              • ava Desktop 14.05.2021 23:53 # 0

                                канал слегка наполнен баянами для буржуйских туристов
                                Ответить

                          • ava KoWe4Ka_l7porpaMMep 15.05.2021 04:29 # 0

                            > стрёмно наверное людей там рядом держать: испортят саркофаг еще

                            Супер Сус регулярно туда катается, пока ничего ещё не испортил.
                            Ответить

                    • ava guest6 14.05.2021 23:15 # 0

                      Какой багор )))
                      Ответить

                    • ava Desktop 14.05.2021 23:21 # 0

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

                    • ava CHayT 14.05.2021 23:21 # +3

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

                      • ava Desktop 14.05.2021 23:23 # 0

                        а ковидных?
                        Ответить

                      • ava bormand 14.05.2021 23:26 # 0

                        Но биологическое оружие вроде запрещено...
                        Ответить

                        • ava CHayT 14.05.2021 23:34 # +2

                          Швейк воевал в первую мировую, тогда ещё не было душнил из ООН с их глубокой озабоченностью.
                          Ответить

                      • ava guest6 14.05.2021 23:27 # 0

                        Проблема вагонетки?
                        Ответить

                      • ava MAKAKA 15.05.2021 01:00 # +1

                        Гашек всё таки охуенный чувак! Сто лет прошло, а как всё актуально до сих пор!
                        Ответить

                    • ava Desktop 14.05.2021 23:21 # +2

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

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

                    • ava gologub 15.05.2021 00:16 # +1

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

                    • ava guest6 15.05.2021 19:42 # +2

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

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

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

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

                  • ava guest6 14.05.2021 23:15 # 0

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

                • ava guest6 14.05.2021 23:14 # 0

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

    • ava MAKAKA 14.05.2021 22:56 # 0

      пиздец Бьёрне старый((
      https://twitter.com/KathrinPetrova/status/1237430865329819648
      Ответить

      • ava gologub 14.05.2021 23:00 # 0

        даже подписать не поленились
        а розетки присобачили криво
        https://pbs.twimg.com/media/ESw8tKCWoAEgewe?format=jpg&name=large
        котлин, хули
        Ответить

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