1. Python / Говнокод #27361

    +1

    1. 01
    2. 02
    3. 03
    4. 04
    5. 05
    6. 06
    7. 07
    8. 08
    9. 09
    10. 10
    11. 11
    12. 12
    13. 13
    14. 14
    import cowsay
    cowsay.cow('Hello World')
    
    
      ___________
    < Hello World >
      ===========
                    \
                     \
                       ^__^
                       (oo)\_______
                       (__)\       )\/\
                           ||----w |
                           ||     ||

    Запостил: 3_dar, 15 Апреля 2021

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

    • ого
      этак ты скоро banner откроешь
      Ответить
    • Это, надеюсь, из стандартной либы?
      Ответить
    • Мууукни
      Ответить
      • Звучит как очередное фурри-порно с фуррхаба.
        Ответить
    • Законтрибьють шаблоны со свиньёй и петухом.
      Ответить
      • Питон же поддерживает юникод в идентификаторах!
        pigsay.хрюкни('Hello World')
        Ответить
      • Хорошая идея, кстати.
        Ответить
        • Можно будет потом показывать на собеседованиях свой вклад в опенсурс.
          Ответить
      • >>> cowsay.char_names
        ['beavis', 'cheese', 'daemon', 'cow', 'dragon', 'ghostbusters', 'kitty', 'meow', 'milk', 'pig', 'stegosaurus', 'stimpy', 'turkey', 'turtle', '
        tux']

        Свиния уже есть :(
        >>> cowsay.pig("Hello GK!")
          _________
        < Hello GK! >
          =========
                      \
                       \
                        \
                         \
                                   ,.
                                  (_|,.
                                  ,' /, )_______   _
                              __j o``-'        `.'-)'
                              (")                 \'
                              `-j                |
                                  `-._(           /
                                      |_\  |--^.  /
                                  /_]'|_| /_)_/
                                      /_]'  /_]'
        Ответить
        • это же PryzcheSoft Agent!
          Ответить
          • Over 50M+ Successfully Migrated User Mailboxes
            Priasoft specializes in complex Exchange and Office 365 Migration to the Microsoft Cloud or Cross-Forest. We can handle any Exchange or Office 365 Migration scenario.


            Cross-Forest, On-Premises Exchange Migration
            Mergers and Acquisitions
            Source and target Exchange environments are in separate AD forests

            Learn more →


            On-Premises to Office 365 Migration
            Transition to the Microsoft Cloud
            Source and On-Premises Exchange syncs with Office 365

            Learn more →


            Same Forest, Cross-Domain Exchange Migration
            IT Modernization and Upgrades
            Source and target Exchange servers are in different domains but same forest

            Learn more →
            Ответить
            • More than just a POS, you think ECNESOFT

              ECNESOFT is a not ‘package’ software that tries to apply a single generic so-lution to all types of industries. ECNESOFT comprises of multi-modular solu-tions that specifically target the retail, restaurant, and stock based businesses.
              Ответить
              • My system is getting slow. What should I do?

                A.

                We recommend our customers to reset system when the system has been used for more than one year.
                Ответить
                • А если год ещё не прошёл, а она уже тупит?
                  Ответить
                • звучит как саппорт макрософага, где индус Раджеш советует тебе либо переустановить венду, либо обратиться к производителю компьютера
                  Ответить
                  • еще советует sfc /scannow
                    Ответить
                    • На всякий случай напомню, что ты общаешься со Стертором (aka уёбком).
                      Ответить
                      • ­ __________________
                        < Не отвечай уёбку >
                         ------------------
                            \
                             \  /\/\
                               \   /
                               |  0 >>
                               |___|
                         __((_<|   |
                        (          |
                        (__________)
                           |      |
                           |      |
                           /\     /\
                        Ответить
                      • Это ты про меня или Гологуба?
                        Ответить
                    • Ещё из забавных советов есть "перерегистрировать все dll'ки". И он пару раз реально помогал на каких-то убитых тачках.
                      Ответить
                      • и winsock resetнуть
                        Ответить
                        • вы так щас договоритесь до того, что MVР из Гуджарата полезные вещи советуют
                          хотя не исключено, что ECNESOFT SO-LUTIONS так и возникла
                          Ответить
                        • А это часто помогало кста. Останки старых дров мешали, походу.
                          Ответить
                          • сброс винсока и перерегестрация комов?

                            Каталог винсока* вроде уже прокляли и начиная с висты там другой API)
                            А ком могли перерегистрировать в рамках dll hell, да


                            *
                            https://en.wikipedia.org/wiki/Layered_Service_Provider
                            Ответить
                            • Ну я про времена ХР, само собой. В семёрке и выше я таких проблем не помню. Может быть просто ебанутые сборки никто уже не делал...
                              Ответить
                              • В семерке все таки стали лучше юзать WinSxS, так что dll hell отступил (ну и кома стало меньше), и LSP стали меньше пользоваться из за перефигачивания сетевого стека
                                Ответить
                          • не дров, это юзермод для тех, кто слишком ленив и анскиллен для написания NDIS или фильтра
                            впрочем на фильтры там тоже есть строгое ограничение
                            Ответить
        • Могут ли возникнуть проблемы с добавлением «cock»?
          Ответить
    • ­ ______________________
      < Столлман - насильник >
       ----------------------
           \
            \
                   ,;;;;;;;,
                  ;;;;;;;;;;;,
                 ;;;;;'_____;'
                 ;;;(/))))|((\
                 _;;((((((|))))
                / |_\\\\\\\\\\\\
           .--~(  \ ~))))))))))))
          /     \  `\-(((((((((((\\
          |    | `\   ) |\       /|)
           |    |  `. _/  \_____/ |
            |    , `\~            /
             |    \  \           /
            | `.   `\|          /
            |   ~-   `\        /
             \____~._/~ -_,   (\
              |-----|\   \    ';;
             |      | :;;;'     \
            |  /    |            |
            |       |            |
      Ответить
    • Признавайтесь, кто?

      https://imgur.com/xfBXxqj
      Ответить
      • Добрый вечер. Файк, завтра бухаем?
        Ответить
      • Файк, ну сходи уже побухать :с
        Ответить
        • Это вредня (*  ̄︿ ̄)!
          Ответить
        • Набухаются перед перелётом Файка и не того в самолёт до голландии запихают...
          Ответить
          • https://www.youtube.com/watch?v=dQWFGUcNkM4
            Ответить
            • Файк, ты именно алкоголь не хочешь или общаться? Хочешь я тоже не буду пить? Приходи.
              Ответить
              • созвонитесь по скайпу
                Ответить
                • Не используйте несвободное программное обеспечение! (︶︹︺) Созвонитесь в Matrix.
                  Ответить
                  • P.S. Забавная история про Skype, которую мне рассказал бывший сотрудник: M$ купил его джважды. Поскольку при первой покупке CEO скромно умолчал, что патенты и права на P2P протокол в сделку не входят.
                    Ответить
                    • какой багор )))
                      Ответить
                    • похоже на херню, как будто на рынке у цыган этот 5куре покупали
                      Ответить
                      • Так они евреи вроде... Или евреи были в "ICQ"?
                        Ответить
                        • ICQ. Мирабилис компания назывлась.

                          Скайп это эстонцы, шведы и датчане
                          Ответить
                        • а MSFT в данной ситуации - руские, которых евреи заставили водку пить, чтоб рускую землю дешевле купить
                          https://www.youtube.com/watch?v=0Qeu8TEBvJ4
                          Ответить
                    • Мы конечно же поверим
                      Ответить
                  • Ты кстати зачем из #govnokod:matrix.org ушел?
                    Ответить
                • Нахуя?
                  Ответить
              • общаться. и вообще у меня сейчас эпизод уже больше полумесяца.
                Ответить
                • Слив защитан.
                  Ответить
                  • ебать, ты только сейчас понял?
                    Ответить
                    • Файк, не ломайся

                      Пойдем в шумную компанию, увидишь много незнакомых людей, весело же
                      Ответить
                      • ты так говоришь, будто я это себе не представляю
                        Ответить
                        • Открою тебе секрет, я тоже поехавший. Меня, наример, нечего бояться.
                          Ответить
                          • Да на гк вообще одна психиатрия. Один Стертор чего стоит.
                            Ответить
                          • ты так говоришь, будто я это себе не представляю
                            Ответить
        • достаточно найти ханурика с горящими трубами, базово обучить мемасам говнача и подослать к ним
          если ханурик представится файком то это даже не обман будет
          Ответить
    • Я сегодня хотел изучить алгоритм Дейкстры... Когда я начал писать на питоне, я осознал, насколько он хуёв в плане изучения алгоритма Дейкстры. Алгоритм Дейкстры требует: два массива, два типа: ребро и вершина... Когда я подумал, что мне нужно будет это всё закодить, я расстроился и просто прочитал дальше книгу.

      Затем я захотел изучить алгоритм обход в ширину, ну и тут мне снова стало лень писать графы и всю эту питушню...

      Вот совсем недавно я сел писать структуру данных КУЧА, но на этот раз подошёл к этому умнее. Я решил использовать язык программирования «C++». Я сел, начал писать, создал проект в ЕМАКСЕ. И что бы вы думали! Я решил, что плохо просто написать кучу, нужно написать абстрактный шаблонный класс Heap, от него наследовать два шаблонных класса MinHeap и MaxHeap, впилить туда умные поинтеры, ещё что-нибудь умное... И мне так стало лень, что и кучу я не написал.
      Ответить
      • Именно поэтому я за "Си". Там ничего не отвлекает от алгоритма и данных.
        Ответить
        • А что насчёт паскаля?
          Ответить
          • Тоже сойдёт, главное не бери делфи чтобы на гуйню не отвлекаться.
            Ответить
            • вредный совет же
              я в ночь с пятницы на субботу такое слепил прямо в фаре на полтора экрана
              адское количество времени ушло только на всяко Lenght и прочие несбаландированные скобки
              ну и отладка сам понимаешь какая
              Ответить
            • > не бери делфи

              Правильно, он уже зашкварен осетинским уёбком
              Ответить
          • именно по этому я за
            https://www.ozon.ru/product/algoritmy-i-struktury-dannyh-128290/
            Ответить
      • > MinHeap и MaxHeap

        Нафиг? Это ж просто замена компаратора.
        Ответить
        • Всё равно два класса получатся, с разными компараторами, т.к. суть кучи в том, что она хитро расставляет элементы по массиву и потом его перебирает, когда что-то туда добавляет или удаляешь.

          Будет как минимум неэффективно переобувать кучу заменой компаратора за nlogn время...
          Ответить
          • Хотя, кстати, написать кучу, использовав паттерн dependency injection, чтобы в неё встроить компаратор на этапе инициализации, будет полегче.

            Можно ещё сделать фабричный метод, который возвращает либо такую, либо другую кучу.
            Ответить
          • Шаблонизируй структуру компаратором, раз уж ты всё равно в шаблоны нячал упарываться.
            template<typename T, typename Comparator>
            struct Heap {
            // ...
            if (Comparator{}(element_a, element_b)) { /* element_a < element_b */ }
            // ...
            };
            template<typename T>
            using MinHeap = Heap<T, std::less<T>>;
            template<typename T>
            using MaxHeap = Heap<T, std::greater<T>>;
            Ответить
      • > Я решил, что плохо просто написать кучу, нужно написать абстрактный шаблонный класс

        YAGNI
        Ответить
        • И KISS!
          Ответить
          • https://dev.by/news/intervyu-s-krisom-kasperski-aka-mysch-h

            > Одну текущую задачу сначала показали «плюсовику», спросив, сколько займёт её решение. Он сказал: «Здесь нужно писать могучий движок. Короче говоря, это проект на полгода». Его коллега-«сишник» поинтересовался: «А зачем?» Ведь поставленная задача укладывается в сотню строк кода! Ответ был ошеломляющим: «Ну и что, мы так и будем по сотне строк кода писать для решения частных задач, каждый раз, как они возникают? Нетушки, задачи надо решать раз и навсегда!».

            > По моему глубокому личному убеждению, проблемы нужно решать по мере их возникновения. Писать программы на вырост с избыточным универсализмом нужно лишь очень хорошо предварительно подумав, ибо это из серии «Почему сегодня не делают корабли, летающие к звёздам?» Ответ прост: потому что корабль, построенный завтра, прибудет быстрее, а корабль, построенный послезавтра, еще быстрее. И их обоих обгонит корабль, построенный лет через пятьдесят, но когда он вернётся обратно, то обнаружит, что у человечества совсем другие проблемы».

            Поэтому я за Си.
            Ответить
            • При всем уважении к Крису как к хакеру и знатоку лоу-левел пижни: Крис не писал больших сложных и унылых энтерпрайзов, и не видел как двести питухов двести раз написали сто одинаковы строк кода.

              А тот, кто это видел, сразу попытается обобщить задачу.
              Ответить
              • При изучении программирования обобщать точно ничего не надо от слова совсем. ОП признался, что зубрит алгоритмы, и это значит, что поначалу он неминуемо будет писать говно, пока не прокачается. Не советую ни с шаблонами, ни с классами на этом этапе соприкасаться. Знать, что они есть, надо, а пользоваться — не надо. Иначе вместо исправления и улучшения говна всё время уйдёт на абстрагирование говна, и мир увидит ещё одного Java Middle.
                Ответить
                • Я писал про комментарий Криса.

                  В случае обучения действительно лишние абстракции не нужны: нужно сосредоточиться на том, что ты изучаешь. И лучше всего делать это чистых сях или паскале
                  Ответить
                  • Мне ещё хочется на собеседовании показывать гитхаб с хитровыделанным кодом: с классами, шаблонами и лямблиями.
                    Ответить
                    • Ну такое... Если мне джун на собесе покажет гитхаб с хитровыебанным кодом, вместо рабочего, покрытого тестами кода, выполняющего какую-то задачу, это будет не слишком эффектно.
                      Лучше на тесты налегай, куда полезнее.
                      Ответить
                      • И coding style сделай стандартный и приятный, ибо всратый код никто читать не будет.
                        Disclaimer: мои советы распространяются только на конторы адекватов.
                        Ответить
                      • /me ушла удалять свой гитхаб
                        Ответить
                        • Ты на ждуна собралась собеседоваться что ли?
                          Ответить
                          • Ждун, это который ждёт, пока Qt Boost Enterprise проект скомпилируется?

                            Или который написал числодробилку на скриптушне, и ждёт результат?
                            Ответить
                            • Который написал N+1 при работе с SQL.

                              Ожидание: Лолечка, в твой первый рабочий день тебе нужно найти кротчайший путь между узлами графа самым оптимальным образом

                              Реальность: А умеешь иконку на сайте поменять?
                              Ответить
                              • если человек знает как грааф обойти то иконку точно поменять сможет

                                а если еще и про проектирование приложений читал то и статику иконки правильно разместит
                                Ответить
                              • > Реальность: А умеешь иконку на сайте поменять?

                                Ну так не выбирай такую реальность, если совсем с голоду не помираешь...
                                Ответить
                                • >не выбирай такую реальность

                                  А я все думал почему тут столько анимешников
                                  Ответить
                                • Ну это reductio ad absurdum конечно, но я пытался сказать, что для джуна в небольшом городе Лолечка как-то мощно замахнулся
                                  Ответить
                          • > ждуна

                            А, сеньоритам уже можно писать хитровыебанный код без тестов?
                            Ответить
                            • Они же не пишут код,
                              а только умничают и пют чяй с другими сеньоритами. И хихикают!
                              Ответить
                            • > А, сеньоритам уже можно писать хитровыебанный код без тестов?

                              Ну сеньорита на собесе за свои изъёбы может хотя бы может постоять. А если джун покажет какую-нибудь уберметушню, то собеседующий может получить немало лузлов, спросив, к примеру, "а что будет, если мы инстанциируем твою метушню другой метушнёй с перегруженным оператором & и конструктором, бросающим исключение, но только в Юрьев день".
                              Ответить
                              • > собеседующий может получить немало лузлов, спросив, к примеру, "а что будет, если мы инстанциируем твою метушню другой метушнёй с перегруженным оператором & и конструктором, бросающим исключение, но только в Юрьев день".
                                Senior C++ Developer ня такие хитрые вопросы должен без запинки отвечать: это UB ┐(︶▽︶)┌.
                                Ответить
                                • А если собеседующий спросит: "а почему?", ему можно ответить: "потому что вы не привели пунктов стандарта, по которым ваша метушня, которой вы инстанциировали мою метаметушню не UB".

                                  Шах и мат, сиплюсисты.
                                  Ответить
                      • >Лучше на тесты налегай

                        Решение очевидно: надо писать свой тестовый фреймворк
                        Ответить
                        • > надо писать свой тестовый фреймворк

                          Зачем? Зачем?

                          Унылый бройлерплейт же, никаких особо интересных задач там нет. Одна из тем, которые вообще не хочется велосипедить.
                          Ответить
                          • Можно делать его «в стиле аниме», чтобы интересно было.
                            Ответить
                          • Лолшто, это крайне интересная тема. Stateful и stateless property based testing, shrinking, trace-based testing, model-checking, trace-based testing.
                            Я свой trace-based навелосипедил, кстати, и им даже кто-то кроме меня начал пользоваться.
                            Ответить
                            • > Stateful и stateless property based testing, shrinking, trace-based testing, model-checking, trace-based testing

                              - если в третий раз заняться trace-based testing, будет ещё интереснее!

                              > кто-то кроме меня начал пользоваться

                              - фу, хипстота. Уверен, что они забросили руст ради этого
                              Ответить
                            • А зачем вообще нужен какой-то "testing", если можно формально доказать?
                              Ответить
                              • > если можно формально доказать?

                                ...Дайте мне года два на реализацию пузырька.
                                Ответить
                              • Когда-то давно слышала оценку: X денежных затрат ня няписание ПО, ≈1000*X ня формальную верификацию.
                                Ответить
                                • Когда ня эту проблему няучат нятравать няйросетки, станет дешевле.
                                  Ответить
                                  • > Боровчекер лучше, чем ничего, но это ограниченная хрень, т.к. он автоматический, а автоматически можно проверить только малое подмножество не-Тьюринг полных программ.

                                    > няйросетки, станет дешевле

                                    Сестра, какое решение Вы в итоге предлагаете и для какой проблемы-то?
                                    Ответить
                                  • С вероятнястью 92.16% няша программа работает математически правильня!
                                    Ответить
                                    • ...потому мы принимаем её в качестве прошивки для нового аэробуса. Спасибо!
                                      Ответить
                                      • С удовольствием полечу на аэробусе, корректность прошивки которого была доказана с помощью нейросетей, и прогнана через coqchk.
                                        Ответить
                                        • > была доказана

                                          Но для начала придётся перечитать все формулировки, которые там пытались доказать... А то вдруг там биологическая нейросетка какую-то фигню на входе набросала. И в итоге напруфали какую-то фигню, не имеющую отношения к полёту.
                                          Ответить
                                    • Не совсем так... с вероятностью 92.16% няша нейросетка сможет доказать, что наша программа работает математически правильно. Если доказать не может -- можно ещё погонять или попробовать по-другому обучить. Ну или вручную помочь в конце-концов.

                                      Сам пруфчекер то на нейросетку никто в здравом уме не будет переписывать.
                                      Ответить
                                      • Вот эта сестрёнка правильно говорит. De Brujin principle во все поля: генерить доказательство можно чем угодно, хоть мышиным облучением, хоть ворециями, если потом проверять доказательство строгим доверенным алгоритмом.
                                        Ответить
                                        • Кстати, а насколько большое это самое ядро coq?
                                          Ответить
                                          • https://coq.discourse.group/t/coq-trusted-kernel-code-size/1012
                                            Ответить
                                            • > TCB рассеяно по всей кодовой базе
                                              > 18к строк

                                              Печально как-то...
                                              Ответить
                                              • Ты сомневаешься в том, насколько trusted этот trusted code base?
                                                Ответить
                                                • Ну просто на нёй все пруфы держатся. Если там бага, то можно какую-нибудь фигню надоказывать.

                                                  Хотя, конечно, у тех же крестов или джавы её вообще нет.
                                                  Ответить
                                                  • Посмотри в сторону metamath, или там mm0

                                                    https://www.youtube.com/watch?v=Rst2hZpWUbU
                                                    Ответить
                                                    • https://github.com/digama0/mm0/tree/master/mm0-c - проверяльщик пруфов на сишке.
                                                      Ответить
                                                    • Да обсуждали уже, что metamath ни от каких известных парадоксов не защищает.
                                                      Ответить
                                                      • Как и Coq. На Coq не выйдет доказать полноту и непротиворечивость Coq.

                                                        Гёделем доказано, что ничто от этих парадоксов не защитит.
                                                        Ответить
                                                        • > На Coq не выйдет доказать полноту и непротиворечивость Coq.
                                                          А в чём парадокс?
                                                          Ответить
                                                          • https://govnokod.ru/23305#comment397642
                                                            Ответить
                                                            • Существуют теоремы, которые Coq ня может ни доказать, ни опровергнуть.

                                                              А в чём парадокс?
                                                              Ответить
                                                              • Парадокс в том, что для доказательства Coq нужна другая питушня, которую тоже самой собой не докажешь. В итоге все доказательства на Coq держатся на вере в корректность Coq... Вот такой вот парадокс математики как религии!
                                                                Но это не точно
                                                                Ответить
                                                                • А это глобальняя проблема математики, так работают все современные (мейнстримные) математические теории. При чём тут конкретня Coq — ня ясно.

                                                                  Если j123123 это ня нравится — ему нужня идти в неклассические логики, там люди ведут няравную борьбу с брадобреями, лжецами и гёделями.
                                                                  Ответить
                                                              • Парадокс в том, что Coq не может доказать корректность Coq. И даже если б мог, это б ничего не доказывало, ведь если вдруг Coq некорректен, то доказательство корректности Coq в рамках Coq будет хуйней, а не доказательством.
                                                                Ответить
                                                                • Корректность Coq доказывается нязависимыми от Coq средствами.

                                                                  А в чём парадокс?
                                                                  Ответить
                                                                  • > Корректность Coq доказывается нязависимыми от Coq средствами.

                                                                    Ничем она не доказывается. А даже если б доказывалось, чем бы доказывалось корректность тех средств? А как бы доказывалась коректность средств доказательства средств, и корректность средств для средств для средств и так далее?

                                                                    В этом и парадокс.
                                                                    Ответить
                                                                    • Поздравляю, вы открыли глобальные проблемы современной математики! Няпротиворечивость формальной системы X нявозможня доказать средствами системы X, но можня — средствами другой (ня эквивалентной X) формальной системы Y. Няпротиворечивость Y доказывается в Z, Z — в W, и так до тех пор, пока ня устанешь.

                                                                      Да, Coq может быть противоречив. Но Coq (как формальняя система) противоречив тогда и только тогда, когда противоречивы формальные системы, которыми доказывалась няпротиворечивость Coq — арифметика Пеано, ZFC или что там у них в фундаменте лежало. А это будет ознячать противоречивость вообще всей современной математики. Поэтому твои придирки конкретня к Coq совершення бессмысленны.
                                                                      Ответить
                                                                      • То есть Coq объективно корректен? (Если в нем нет багов).
                                                                        Ответить
                                                                        • Для ответа ня этот вопрос нужны более мощные девочки-волшебницы, прости (。╯︵╰。).

                                                                          Но в общем случае, если няпротиворечивость формальной системы X была доказана в формальной системе Y, то из противоречивости X следует противоречивость Y — классическое доказательство от баки.
                                                                          Ответить
                                                                          • Ну ничего, я бы другого, более мощного, доказательства бы и не понял :-)

                                                                            Спасибо!
                                                                            Ответить
                                                                        • Да, а ещё, как я уже говорила, есть разные няклассические логики. Няпример, паранепротиворечивая*: в ней допускается существование противоречий, что позволяет с некоторым успехом побороться со злыми гёделями. В самом своём основании, теорема Гёделя основывается ня предложении P = "P ня может быть доказано в X", из существования которого делается вывод, что X либо противоречива, либо няполна. Однако в паранепротиворечивой логике возможня существование противоречий: истинных предикатов, для которых также истинно их отрицание, и это ня приводит к противоречивости системы, что делает классические доказательства теоремы Гёделя някорректными.

                                                                          * https://plato.stanford.edu/entries/logic-paraconsistent/
                                                                          Ответить
                                                                          • https://youtu.be/u1AyoXrXYe4?t=1263
                                                                            Ответить
                                                                            • Лучше https://habr.com/ru/post/426033/ и https://en.wikipedia.org/wiki/Inter-universal_Teichmüller_theory. Ярчайший пример кризиса в современной математике.
                                                                              Ответить
                                                                            • wut? вся путинистская рашкокодемия не может блохчейна собрать?

                                                                              каждый раз сoсk-полно убеждаюсь что рашка - это апскейл Tropico 4, где кокодемия нужна только для выращивания клона El Presidente
                                                                              Ответить
                                                                      • > когда противоречивы формальные системы, которыми доказывалась няпротиворечивость Coq

                                                                        Никакими формальными системами непротиворечивость Coq (конкретно реализации этого Coq, написанной на OCaml) не доказывалось. Корректность компилятора и интерпретатора OCaml тоже нихрена не доказывалась.
                                                                        Ответить
                                                                        • Ты путаешь няпротиворечивость формальной системы и корректность реализации. Почитай https://github.com/coq/coq/wiki/Presentation#what-do-i-have-to-trust-when-i-see-a-proof-checked-by-coq.

                                                                          Няпротиворечивость формальной системы Coq доказывается математически, и если она всё таки противоречива, то вся современная математика тоже противоречива.
                                                                          А вот корректность конкретно твоей реализации и корректность твоего железа к Coq как формальной системе в принципе никак ня относятся. Это совершенно другая — тоже рекурсивная, впрочем — проблема, которая в абсолютно равной степени затрагивает вообще любые методы доказательств. В любых системах автоматического доказательства могут быть ошибки. В любых компьютерах могут быть ошибки. Люди, доказывающие теоремы вручную, тоже совершают ошибки.
                                                                          Редуцировать вероятность ошибки до бессмысленности теории — это классический максималистический нигилизм.
                                                                          Ответить
                                                                          • > Няпротиворечивость формальной системы Coq доказывается математически, и если она всё таки противоречива, то вся современная математика тоже противоречива.

                                                                            Кем она доказывается? Мозгом математиков? Как мы можем понять, что мозги математиков корректно работают?

                                                                            >А вот корректность конкретно твоей реализации и корректность твоего железа к Coq как формальной системе в принципе никак ня относятся.

                                                                            А корректность нашего мышления (вычисления, производимые мозгами человеков) относится? Может быть у всех людей некое конгитивное искажение, которое делает всю эту математику полной херней, и все наши рассуждения о корректности или некорректности чего-то там вообще не имеют смысла.
                                                                            Ответить
                                                                            • > Кем она доказывается? Мозгом математиков?
                                                                              Да, по старинке, вручную.

                                                                              > Как мы можем понять, что мозги математиков корректно работают?
                                                                              > Может быть у всех людей некое конгитивное искажение, которое делает всю эту математику полной херней, и все наши рассуждения о корректности или некорректности чего-то там вообще не имеют смысла.
                                                                              Осторожня, у вас резкое обострение нигилизма, возможен аварийный выход из Матрицы!
                                                                              Ответить
                                                                              • > Осторожня, у вас резкое обострение нигилизма, возможен аварийный выход из Матрицы!

                                                                                Я уже давно как.
                                                                                Ответить
                                                                            • > Кем она доказывается? Мозгом математиков? Как мы можем понять, что мозги математиков корректно работают?

                                                                              Поэтому я за `Арнольда': "математика — это раздел теоретический физики, отличие только в том, что в физике эксперименты стоят миллиарды долларов, а в математике — единицы рублей" (точную цитату мог переврать, но суть, нядеюсь, передал).
                                                                              Ответить
                                                                              • Цитата конечно хорошая, только вот не всякая математическая питуля имеет какую-то физическую интерпретацию. Взять например функцию Аккермана - к какой физике она имеет отношение?

                                                                                Не, можно конечно рассмотреть некий компьютер, который считает функцию Аккермана, компьютер это вполне себе физическая штука, и можно решить физическую задачу, хватит или не хватит места на жестком диске такого-то компьютера чтоб посчитать функцию Аккермана с такими-то параметрами, но это как-то сильно натянуто.
                                                                                Ответить
                                                                                • Если доказательство не может быть проверено ничем, кроме проамфетаминенного мозга другого узкоспециализированного математика, то это астрология какая-то.

                                                                                  Суть цитаты я вообще вижу вообще в другом. Что нахождение проверяющего доказательство субъекта или алгоритма в физическом мире, где всё определяется вероятностно, канселлит притязания практически любой формальной системы на непротиворечивость.

                                                                                  Допустим, j123123 наебнул Гёделя и выполнил программу Гильберта на metamath на микроконтроллере. Он утверждает, что его программа на 100% верна, но я тут такой: "а вдруг космическая частица попала в твой микроконтроллер во время проверки доказательства?". На что он: "а я два раза запускал." А я: "а что если два раза попала?"

                                                                                  Вероятность такого события конечно исчезающе мала, но она никогда не нулевая. Вот и получается, что физика кроет любую математику.
                                                                                  Ответить
                                                                                  • > Вот и получается, что физика кроет любую математику.
                                                                                    А вся физика кроется субъективнястью восприятия. j123123 ня выполнил программу Гильберта ня микроконтроллере, ему это просто показалось из-за нядостатка сна. А у тебя просто когнитивное искажение, из-за которого ты ня осциллографе, подключённом к к микроконтроллеру, ня котором якобы выполнялась программа Гильберта, видишь то же, что j123123 видит в своём глюке.
                                                                                    Ответить
                                                                                    • Субъективность восприятия тоже когнитивное искажение. Я однажды с велосипеда приложился, и наблюдал перезагрузку мозга с чистого листа. Весело было, поскольку оказывается что мыслительный процесс может существовать без субъекта. Сложно описать, но именно поэтому я против `личности'.
                                                                                      Ответить
                                                                                      • > Весело было, поскольку оказывается что мыслительный процесс может существовать без субъекта. Сложно описать, но именно поэтому я против `личности'.

                                                                                        Наличие субъектности != наличие личности.

                                                                                        Более того, не факт что субъектность подразумевает наличие какого-то мышления.
                                                                                        Ответить
                                                                                        • > Более того, не факт что субъектность подразумевает наличие какого-то мышления.

                                                                                          Именно поэтому я за «РНР»!
                                                                                          Ответить
                                                                                      • > Я однажды с велосипеда приложился, и наблюдал перезагрузку мозга с чистого листа.
                                                                                        А после этого ты стал девочкой-волшебницей ( ^▽^)?
                                                                                        Ответить
                                                                                        • > А после этого ты стал девочкой-волшебницей ( ^▽^)?

                                                                                          Какой исекай )))
                                                                                          Ответить
                                                                                  • Поэтому вопрос "кто доказал, что имплементация Coq абсолютно верна" довольно непрактичен, а правильный вопрос звучит как "насколько Coq увеличевает вероятность того, что для доказанной с его помощью теоремы не найдётся контрпримера".
                                                                                    Ответить
                                                                              • Шварцняггера?
                                                                                Ответить
                                                                                • https://ru.wikipedia.org/wiki/Арнольд,_Владимир_Игоревич
                                                                                  Ответить
                                                                              • > единицы рублей

                                                                                Математики работают за еду?
                                                                                Ответить
                                                                                • > Математики работают за еду?

                                                                                  Тут имеется в виду, что математику не надо ставить реальные эксперименты, ему достаточно посчитать.
                                                                                  Ваш К.О.
                                                                                  Ответить
                                                                                  • > ему достаточно посчитать

                                                                                    Скажи это математикам, которые работают над криптовалютами.
                                                                                    Ответить
                                                                                • яркий и кошерный пример - Перельман, лол
                                                                                  Ответить
                                                                    • Какой парадокс )))
                                                                      Ответить
                • Это правда. Для изученяя алгоритма сортировки пузырьком нужня писать алгоритм сортировки пузырьком, а не интерпретатор Java-байткода на шаблонах C++.
                  Ответить
              • > А тот, кто это видел, сразу попытается обобщить задачу.

                Ну так я не спорю. Ты обобщаешь тогда, когда это надо обобщать. В той же цитате есть:

                > Писать программы на вырост с избыточным универсализмом нужно лишь очень хорошо предварительно подумав

                Если ты хорошо предварительно подумал, тогда берешь и обобщаешь. А если ты допустим пишешь некий игровой движок, который умеет 2D и 3D графон, и ты такой "бля, надо бы обобщить всё, чтобы можно было и 4D, 5D, 6D и так далее", то это полная херня. Не, есть какие-то экспериментальные четырехмерные игры, но это их раз два и обчелся https://en.wikipedia.org/wiki/List_of_four-dimensional_games
                Ответить
                • Минус – это плюс, я промахнулся.

                  В списке 4D игр есть «2048 4D». Там не одно поле 8х8, а четыре поля 2х2. Какое 4Д )))
                  Ответить
                  • Дык это проекции, наверное? Нельзя взять и нарисовать 4Д в нашем убогом 3Д пространстве на 2Д мониторе.
                    Ответить
                    • https://huonw.github.io/2048-4D/

                      Вот оно. И это точно не проекции, а скорее ворекции, т.к. проекция трёхмерного куба на плоскость – его развёртка – уже будет состоять из более чем четырёх квадратов. Что уж говорить про 4Д, где развёртка будет 100500 квадратов!
                      Ответить
                      • В гиперкубике 2х2х2х2 у тебя 16 элементов. Можно нарисовать их в виде 4 "слоёв" 2х2. Всё норм вроде.
                        Ответить
                        • Если так, то да, можно. Но это уже питушня какая-то, я себе представляю это так:

                          2Д куб (анимекуб) – 4х4 плоскость.

                          3Д куб (автокадкуб) – 6 плоскостей 4х4, каждая соединена с четырьмя другими.

                          4Д куб (хзчезакуб) – ... ещё больше плоскостей 4х4, и каждая соединена с ещё большим количеством других плоскостей.
                          Ответить
                    • Нарисовать можно что угодно, просто мозг не осилит это понять. Нужно расширять сознание
                      Ответить
                  • лучше всего игра 0AD, в десятичном выражении это больше всех
                    Ответить
                • > Ты обобщаешь тогда, когда это надо обобщать.

                  Немного звучит как "хорошее лучше плохого". Без конкретных примеров тяжело говорить)

                  В целом же еще Брукс писал, что (расширяемую) систему сделать чуть ли не в 10 раз сложнее, чем наколенный код
                  Ответить
              • Обобщать или не надо, это управленческая задача. Прикинуть архитектуру проекта, возможные изменения, [i]адекватность клиента, возможность обломать ему хотелки[i], относительную стоимость того или иного подхода. Затем дать задачу: пишем частный случай или обобщаем. Да, возможно придётся всё равно обобщать после того, как уже написали пару частных случаев, как и возможно написать обобщённый вариант, который будет использоваться в одной конфигурации — это риск, на который приходится идти. Случается такое изредка, или постоянно — отличие хорошего годного компетентного управленца от плохого.
                Ответить
      • > Алгоритм Дейкстры требует: два массива, два типа: ребро и вершина...

        Сначала читаешь про матрицу расстояний в википедии, потом берешь двумерный массивчик размером X на X, где X - количество вершин в графе. Дальше просто берешь и реализовываешь этот алгоритм Дейкстры. Никаких двух массивов с ребрами и вершинами не требуется.
        Ответить
        • Тогда будет неэффективно по памяти для разреженных графов, и неэффективно по времени, т.к. в целом операции на матрице имеют бо́льшую ассимптотику, чем на представлении с помощью adjacency-list.
          Ответить
          • Если ты решаешь учебную задачу, тебе должно быть плевать на эффективность.

            К тому же ты можешь сделать интерфейс к своей структуре данных на двумерном массиве, напиши и протестируй алгоритм Дейкстры на такой структуре с таким интерфейсом, потом с точно таким же интерфейсом можешь запиливать свой adjacency-list, и потом бенчмарк можешь запиливать даже, и юнит-тестить одно об другое. Короче, делай MVP и потом улучшай его.

            А потом чтоб еще формально доказать на Coq что и так и сяк одинаково работает
            Ответить
            • Ого! Звучит очень прелестно, надо будет попробовать, когда станет не так лениво.
              Ответить
            • > Если ты решаешь учебную задачу, тебе должно быть плевать на эффективность.

              - пиздец, пиздец
              Ответить
              • Да не, нормально. Реализовать сортировку пузырьком в учебных целях это вполне обычная практика.
                Ответить
              • Выбор оптимальных по времени и/или памяти алгоритмов это вообще отдельная тема, и это конечно тоже полезно знать. Но если ты еще нихуя не умеешь, и задача перемножить матрицу, надо использовать простые наивные алгоритмы, а не всякие сложные алгоритмы реализовывать, которые в BLAS каком-нибудь есть
                Ответить
        • мне кажется, можно соснуть при оче больших графах
          Ответить
          • Можно применять https://en.wikipedia.org/wiki/Sparse_matrix но это конечно уже сложнее будет. Для начала можно просто с матрицей делать, учитывая что это учебная задача, а не какая-то профессиональная продакшен-хуйня для графов.
            Ответить
      • А конец у этой истории вот такой:

        Я смотрю анимешку, ту самую, про девушку напрокат. Там ГГ такой жук кринджа!
        Ответить
      • >шаблонный класс Heap

        ни в питоне ни в плюсах так не делают
        Ответить
        • откуда ты знаешь?
          Ответить
        • На питоне вообще редко делают шаблонные классы
          возможно потому, что в питоне нет шаблонов
          Ответить
          • я бы попросил

            https://www.geeksforgeeks.org/template-class-in-python/
            Ответить
          • > в питоне нет шаблонов

            В джанге есть.
            Ответить
          • Есть имплементации на импорт хуках и модификации AST.
            Ответить
            • Какой у тебя ник?
              Ответить
              • У меня только файки.
                Ответить
              • А что, тебя смущает моя заинтересованность в кодогенерации на питоне?
                Ответить
                • Я просто был уверен, что знаю всех, кто пишет под гостём
                  Но никто их них не кодогенерит на питоне
                  Ответить
                  • Я просто пишу потому что удобно из телеграма. Этот бот опенсорсный? Можно было бы себе поднять для неанонимного постинга комментов на ГК.
                    Ответить
                    • Зерегайся на govnokod.xyz, далее можно залогиниться в боте командой /login
                      Ответить
                      • О, спасибо. Там ссылка верификации для синка с ру не работает, если подключен по https. Какой багор)))
                        Ответить
      • лол
        https://www.python.org/doc/essays/graphs/
        Ответить
    • https://twitter.com/TheMFingCOO/status/1383787974022762505?
      Ответить
      • Та зелёная телка, самая шарообразная, мне напомнила Майка Вазовского.
        Ответить
        • не уверен, что это тётка
          Ответить
          • Девочка-няшечка миленькая неформалочка?
            Ответить
          • Кстати да, жирное аморфное тело с гормональными нарушениями – идеал идей западного либерализма, ведь по нему не скажешь, тетка это или мужик: через слои жира пруфы не разглядеть, а стремление тела к сферической форме убирает всякую возможность ассоциировать человека с тем или иным полом.
            Ответить
            • >стремление тела к сферической форме
              Хочу стать смешариком.
              Ответить
            • Понятно. Это чтобы когда ебешь колобка не понимая куда ты ебешь в какую складку и не понимаешь гей ты или нет.
              Ответить
        • Private Eye Вазовский
          Ответить
    • Бох забери у них жизни - они их в пустую стратят
      Ответить
    •   ___________
      < I'm a bull! >
        ===========
                      \
                       \
                        c^__^э
                         (фф)\_______
                         (__)\       )\/\
                             ||---/- |
                             ||     ||
      Ответить

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