Сохранен 165
https://2ch.hk/pr/res/347589.html
Из-за проблем с продлением домена ARHIVACH.NET, с 13 октября он может перестать функционировать. В связи с этим Архивач временно переходит на использование прежнего домена ARHIVACH.NG.
Напоминаем, что сайт всегда доступен через Tor по адресу arhivachovtj2jrp.onion. Установите Tor Browser для беспрепятственного доступа!
Аноним Птн 25 Апр 2014 23:25:21  #1 №347589 
[url]

Всем гомотопий, поцоны.

Loading...
Аноним Суб 26 Апр 2014 00:08:51  #2 №347605 

>>347589
Какой хуйней только люди не занимаются.

Аноним Суб 26 Апр 2014 00:17:35  #3 №347611 

>>347605
Забавно.

sageАноним Суб 26 Апр 2014 00:21:22  #4 №347612 

>>347605
Тоже самое подумал. Практическое применение этой хуйне едва ли найдется скоро.

Аноним Суб 26 Апр 2014 00:27:52  #5 №347615 

>>347612
Это лекториум, для них это вполне нормально.

Аноним Суб 26 Апр 2014 00:27:53  #6 №347616 

>>347589
Джява-девелопер на 1:40 вообще в ахуе.

Аноним Суб 26 Апр 2014 02:19:47  #7 №347659 

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

sageАноним Суб 26 Апр 2014 02:51:39  #8 №347672 

>>347659
Ну давай, найди этому применение где-нибудь за пределами учебных заведений.

Аноним Суб 26 Апр 2014 03:12:41  #9 №347680 

>>347615
Блядь, они же там образование должны получать, а занимаются хуйней. Почему так? Рашкованское образование?

Аноним Суб 26 Апр 2014 03:30:27  #10 №347682 

Типичный программач. Эта хуйня, из которой вы, скорее всего, не поймете не слова, используется в математической логике, PLT и теории типов. В частности, развитие примерно похожих областей алгебры и применении их к PLT дало начало пруфчекерам и самопишущемуся коду. Да-да, быдломакака, скоро все эти sql-запросы будут генерироваться самостоятельно, а ты станешь не нужна и пойдешь на биотопливо

Аноним Суб 26 Апр 2014 03:36:27  #11 №347683 

>>347682
>ни слова
>применение их
/fix

Аноним Суб 26 Апр 2014 06:03:47  #12 №347698 

>>347682
Главное, чтобы мамка раньше не померла, а то без борща ноги протянешь и светлого будущего не увидишь.

Аноним Суб 26 Апр 2014 06:58:34  #13 №347700 

когда терию множеств под прувчекеры перепишут?
где гоказательство теоремы феерма под прувчекером?

Аноним Суб 26 Апр 2014 07:41:04  #14 №347701 

>>347700
Сам этого не сделаешь - никто за тебя не сделает.

Аноним Суб 26 Апр 2014 10:50:13  #15 №347726 

>>347682
> скоро все эти sql-запросы будут генерироваться самостоятельно
из чего генерироваться будут?

Аноним Суб 26 Апр 2014 10:50:26  #16 №347727 

>>347672
>>347680
Вообще-то топология применяется в современной физике, химии, астрономии, биологии, теории управления, биоинформатике и даже в программировании (топологическая теория графов, например). Топология - это просто геометрия, из которой удалили понятие расстояния.
>>347682
Ты ошибаешься, топология имеет весьма опосредованное отношение к теории категорий. Хотя общая тенденция есть: топология - это геометрия, где изучаются свойства объектов без учета расстояния, теория категорий - экстремальный вариант математики, в котором полностью абстрагируются от структуры объектов. Это естественно для нормальных программистов - абстрагироваться от каких-то частных свойств объектов с целью написания обобщенных алгоритмов. Естественно, быдлу, не знающему Хаскель, да и просто ОО-быдлу, использующему языки с сабтайпингом и приведением типов такой подход чужд. Даже если было и пытается использовать абстракции, они
1. не несут семантического смысла, типа "всё есть объект".. ну и что? Что это нам даёт? Или "здесь мы используем контроллер" - а какими свойствами он обладает?
2. либо играет в абстракции, когда например апкастит объекты, чтобы якобы абстрагироваться от несущественных свойств, и тут же даункастит их в другом месте программы, т.е. фактически страдает хуйнёй и запутывает код.

Аноним Суб 26 Апр 2014 11:27:52  #17 №347732 

>>347727
ты слабо представляеш себе возможности языка C в области абстрактного программирования

Аноним Суб 26 Апр 2014 11:34:20  #18 №347733 

>>347727
> Топология - это просто геометрия, из которой удалили понятие расстояния.
Ну нет, топология - это непрерывность. Её изучают отдельно как в геометрическом контексте (отрывая от геометрии понятие расстояние), так и в алгебраическом (не знаю, что написать тут умного).
> теория категорий - экстремальный вариант математики, в котором полностью абстрагируются от структуры объектов
Абстрагируются от содержания, а структуру оставляют и изучают.
> да и просто ОО-быдлу, использующему языки с сабтайпингом и приведением типов такой подход чужд
Необязательно, есть вон ОО-категорищки. Дело не в этом. Это как кастанедовское "смотреть" vs "видеть" (возможно, на языке оригинала это противопоставление звучит удачнее), при том, что никакой насущной мотивации для открывающихся возможностей нет.
> Или "здесь мы используем контроллер" - а какими свойствами он обладает?
Определение (в контексте конкретного подхода) перечитать пробовал? То, что ты не знаешь, как сформулировать то же самое формально на языке ТТ или ТК значит лишь, что есть чем заняться.
> естественно для нормальных программистов - абстрагироваться от каких-то частных свойств объектов с целью написания обобщенных алгоритмов.
Это естественно немногим, остальным это неестественно, а так как платят им не за это, то и делать этого они не будут, не умеют, и не хотят уметь.

Аноним Суб 26 Апр 2014 11:52:17  #19 №347737 

>>347672>>347680
На википедию сходите, уебки безмозглые.
>>347682
>когда терию множеств под прувчекеры перепишут?
http://coq.inria.fr/V8.2pl1/contribs/ZFC.html
>где гоказательство теоремы феерма под прувчекером?
Нужен человек, который умеет пользоваться прувером и испытывает глубокую симпатию к теории чисел, а эти множества редко пересекаются, поскольку находятся на противоположных уровнях абстракции.
>>347727
>2. либо играет в абстракции, когда например апкастит объекты, чтобы якобы абстрагироваться от несущественных свойств, и тут же даункастит их в другом месте программы, т.е. фактически страдает хуйнёй и запутывает код.
Чем это отличается от (Mu . unMu) для рекурсии на тайплевеле? Проблема не в запутывании кода, а в динамическом петушении.

Аноним Суб 26 Апр 2014 11:59:42  #20 №347739 

>>347727
>в современной физике, химии, астрономии, биологии, теории управления, биоинформатике
Это имеет какое-то отношение к /pr/, астроном ты наш?

>программировании (топологическая теория графов, например)
Хорошо, сейчас ты мне расскажешь, как можно применить это в программировании, при условии что программа не нацелена изначально на расчеты математического говна.

Аноним Суб 26 Апр 2014 12:04:00  #21 №347740 

>>347737
http://coq.inria.fr/V8.2pl1/contribs/ZFC.html
а теореммы все кто будет забивать?

Аноним Суб 26 Апр 2014 12:26:02  #22 №347743 

>так как платят им не за это, то и делать этого они не будут, не умеют, и не хотят уметь.

Суть местного быдла, бугуртящего на высших эльфов программирования. Зачем что-то учить, вон в пхп все просто и понятно, берешь фреймворк, пишешь гостевуху, PROFIT.

Если ты не интересуешься ТК, топологией, теорией групп, а так же не интересуешься CS'ом, не пишешь на Haskell/Mercury/Coq, ты никакой не программист, а просто гнида слесарь, специально обученный петушок.

!!zunHIrSt Суб 26 Апр 2014 12:42:43  #23 №347750 

>>347743
Проблема в том, что программистам это и не надо, так что такие предъявы к ним несостоятельны. Лучше перестать считать себя В ДУШЕ программистами и изолироваться в какую-то самостоятельную маргинальную единицу, чем пытаться переопределить слово "программист".

!!zunHIrSt Суб 26 Апр 2014 13:08:52  #24 №347753 

Раз уж такой тред, вброшу индейской мудрости: http://pastebin.com/J4AeLCUb

Аноним Суб 26 Апр 2014 13:18:21  #25 №347756 
1398503901977.jpg

http://qps. ru/xts1A
Этoй хуйнe нeт никaкoгo примeнeния, лoл. Чистo зaбaвa для быдлa, кoтoрoe будeт учить всe этo гaвнo для нихуя в сooтвeтствии с кaпризaми кучки мaтeмaтикoв. Типичнoe рaшкoвaнскoe oбрaзoвaниe. Сплoшныe бeспoлeзныe прeдмeты.

>>347727
>Вooбщe-тo тoпoлoгия примeняeтся в сoврeмeннoй физикe...
И eщe в aнусe твoeй мaмки, кoгдa eё кишки вывoрaчивaeт oт мoeгo хуя и нужнo рaссчитaть их oтoбрaжeниe, шкoльник ты eбaнный.

>>347682
>нaбoр слoв кoтoрый сaм нe пoнимaeт
Высрaл нa тeбя змeйку, шкoльник.

>>347737
>Нa википeдию схoдитe, уeбки бeзмoзглыe.
Вижу ты тaм вooбщe рeдкий гoсть.

Аноним Суб 26 Апр 2014 13:26:57  #26 №347760 

>>347753
>Карлос Кастанеда
Проиграно. С такими предрассудками только в дауны, лол.

Аноним Суб 26 Апр 2014 13:38:39  #27 №347764 

>>347756
>гуглит на русском
>считает, что на западе топологии не обучают
>имеет в виду русскую википедию
Заведи себе трипкод уже, чтобы сразу было понятно, что ты дегенерат.

Аноним Суб 26 Апр 2014 13:40:17  #28 №347765 

>>347756
Бугурт неотесанного говнаря из под шконки.
Это теория - будущее, каждый кто работает в этой сфере - открыватель и творец.

А ты, петушок, просто слесарь - человек не способный к абстрактному мышлению, везде желающий увидеть ко-ко-ко применение по месту, говно в общем, а не программист.

!!zunHIrSt Суб 26 Апр 2014 13:48:02  #29 №347767 

>>347760
> С такими предрассудками только в дауны, лол.
Лучшая самореференция за последнее время.

Аноним Суб 26 Апр 2014 13:56:15  #30 №347770 
1398506175421.jpg

>>347764
>я опять обосрался
http://en.wikipedia.org/wiki/Homotopy
Ни одной строчки о реально полезном практическом применении.

>считает, что на западе топологии не обучают
Лол, я понял бы, если бы такой хуйней занимались в узком кругу математиков, но если ей занимаются еще и студенты...
Это просто пиздец.

>>347765
>Это теория - будущее, каждый кто работает в этой сфере - открыватель и творец.
>Смотри как я могу делать выводы из нихуя! Азазаза))))
В твоем маня-мирке, может и так, и может даже в реальность так, но сейчас все местные кукаретики тупо слились без аргументов в пользу полезного практического применения теории в текущий период времени.

Аноним Суб 26 Апр 2014 14:01:07  #31 №347772 

>>347770
>текущем периоде времени.
Слоуфикс.

Аноним Суб 26 Апр 2014 14:05:54  #32 №347773 

>>347767
Забавный клоун, продолжай.

Аноним Суб 26 Апр 2014 14:09:06  #33 №347774 

>>347737
> Чем это отличается от (Mu . unMu) для рекурсии на тайплевеле?
Не, ну он же совсем про другое говорит.
(Mu . unMu) -- локальный костыль, у которого есть конкретное назначение, а апкасты/даункасты порой используются неразумно, где проще было сразу использовать сдаункащенный объект.

Аноним Суб 26 Апр 2014 14:15:13  #34 №347776 

>>347770
нахуй иди

Аноним Суб 26 Апр 2014 14:19:50  #35 №347779 

>>347770
> http://en.wikipedia.org/wiki/Homotopy
> Ни одной строчки о реально полезном практическом применении.
На страничке про производную тоже будешь искать "реально полезное практическое применение"? Это самое базовое понятие большой области математики -- очевидно, что оно нужно, чтобы построить другие понятия.

Аноним Суб 26 Апр 2014 14:29:23  #36 №347782 
1398508163565.jpg

>>347779
Лол, ну поясни тогда коротко о практическом применении теорем, построенных на этой теории гомотопий.

>>347776
Первый готов.

Аноним Суб 26 Апр 2014 14:53:29  #37 №347790 

>>347770
Сегодняшняя теория - завтрашняя практика, ебать если ты не понимаешь.

Поэтому теоретическая математика/физика всегда была и будет куда важнее, чем практическое их направление, потому что теория впереди. Теория - это открытия, практика - надрачивание по выведенным формулам.

Аноним Суб 26 Апр 2014 15:22:41  #38 №347801 

>>347782
В общем, даже лень тебе что-то объяснять.
Таких, как ты — миллионы, серых и отвратительных, как плевки на асфальте. Приходящих сюда ежедневно с ведром грязной воды, которой мыли полы, вместо мыслей.

Аноним Суб 26 Апр 2014 15:52:23  #39 №347813 

а когда Ньютон придумал механнику уже было интегральное ичисление?

Аноним Суб 26 Апр 2014 16:26:56  #40 №347828 

>>347801
>В общем, даже лень тебе что-то объяснять.
Ну хуле, обосрался, а теперь что-то объяснять лень, да.
Второй готов. Славный день для унижения школьников.

Аноним Суб 26 Апр 2014 16:28:42  #41 №347830 

>>347790
>Лол, я понял бы, если бы такой хуйней занимались в узком кругу математиков, но если ей занимаются еще и студенты...
Это просто пиздец.
А вот это было для кого написано, питушочек? Иди кудахтай дальше, долбоеб.

sageАноним Суб 26 Апр 2014 16:43:58  #42 №347836 

>математика
>практическое применение
Лоллировал с дебилов. Математика не имеет никакого отношения к "окружающей реальности" и соответственно "практике". Если какие-то из выводов математики и можно "применить на практике" - то это чистое совпадение, ниодному (нормальному) человеку и в голову не прийдет ставить перед математикой задачи "практического применения".

Аноним Суб 26 Апр 2014 16:49:59  #43 №347838 

>>347836
Ты не умеешь в иронию.
Все как описал, за исключением элементарной математики и Матана.

Аноним Суб 26 Апр 2014 16:51:45  #44 №347839 

>>347836
Физики и инженеры постоянно ставили перед математиками такие задачи, и математики доставяли, обеспечив потрясающий успех науки в двадцатом веке. Правда, с появлением раков под названием "теория струн" и "теория языков программирования" ни о какой практике речи нет, вещь сама по себе.

Аноним Суб 26 Апр 2014 17:08:26  #45 №347846 

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

Аноним Суб 26 Апр 2014 17:13:36  #46 №347847 

>>347846
Еще один униженка. Хуйни-то понаписал, школьник. Иди к себе в поместеье, Элита ты усадебная блядь. Элементарную вещь доказать не можешь, а кукарекаешь про элиту.

Аноним Суб 26 Апр 2014 17:14:18  #47 №347848 

>пля поцоны там какието термины непонятные
Хуевое видео от пхп-дебилоидов для школьников 2-го "Б".
А этот тред - сборище пыхопидоров с гостевухами и быдлостудентов своих мухосранских шараг, которые знают только как написать laba1 на паскале и laba2 на говняшной.

Аноним Суб 26 Апр 2014 17:14:35  #48 №347849 

>>347830
А, то есть, то что студентов учат передовым направлениям, а не какому нибудь старому говну типа теории множеств или матану, тебя смущает. Ну там иди сдохни тогда от рака всего, имбецил опущенный.

Аноним Суб 26 Апр 2014 17:21:51  #49 №347853 

>>347839
Ты все перепутал, ебанашка. Математика и физика способны, и развиваются сами по себе, без всяких запросов, потому что быдло из инженерных специальностей и не знает что запрашивать-то, большинству достаточно и уровня 200-летней давности. И как правило, конкретные специальности юзают уже созданные давно теоремы, подстраивая их под свою быдло область. Так как математика изучает идеальные абстрактные объекты, её теоремы годятся одинаково для всего. Так вот, это теоретические направления физики и математики двигают мир, а не мир двигает их.

Аноним Суб 26 Апр 2014 17:22:41  #50 №347855 

>>347847
Быдлокодер познал выражение "Моча в голову ударила" совершенно буквально. И теперь, валяясь в луже мочи и собственных испражнений, мучаясь приступом шизофазии, он подумал что все-таки надо было оставаться в своем уютненьком мирке с задроченым спектрумом, фабриками адаптеров и тестами на тесты, а не лезть в кодач в непотребном и пьяном виде.

Аноним Суб 26 Апр 2014 17:23:32  #51 №347856 

Спор адептов черного и адептов белого. НАЙС.

Аноним Суб 26 Апр 2014 17:46:26  #52 №347874 

Вот к примеру, Haskell - современный ЯП, с замечательной системой типов, использует последние достижения современной математики - ТК, и ещё есть прекрасные языки с зависимыми типами, использующие HoTT. Новинки, по своему.

Но тебе, быдлу, это не надо, тебе бы на заводе на убогом железе как бы байты похитрее выебать для твоей "инженерной задачи". Тебя вполне устраивают технологии 40-летней давности, а на все новое ты фыркаешь типа "борщехлебы, нахуй надо, говно без задач, вот я на сишечке пок-пок".

Ну ничего, это все вопрос времени, ФП уже повсюду, скоро и тайпклассы подтянутся, а через лет 10, "что такое монада?" - будет стандартным вопросом на собеседовании, хочешь ты того или нет, слесарь.

Аноним Суб 26 Апр 2014 17:49:42  #53 №347876 

Так и математика. Сегодня какие-то направления "без задач", "экспериментальные", а завтра их ставят на пьедестал, выбрасывая оттуда залежавшееся старое говно, типа теории множеств.

Аноним Суб 26 Апр 2014 17:50:06  #54 №347877 

>>347874
>последние достижения современной математики
>ТК
ясно
>Тебя вполне устраивают технологии 40-летней давности
это все которые есть сейчас?
> ФП уже повсюду
и на кухне и в ванной
>тайпклассы подтянутся
понятно
>через лет 10, "что такое монада?
massyv

Аноним Суб 26 Апр 2014 18:00:23  #55 №347880 

>>347877
Странно, что ты пишешь это, печатая одной рукой и сжимая бомбанувший пукан другой.

Аноним Суб 26 Апр 2014 18:47:32  #56 №347894 

>>347782
> Лол, ну поясни тогда коротко о практическом применении теорем, построенных на этой теории гомотопий.
Ну например HoTT, который позволяет лучше формализовать / расширить возможности пруф ассистантов, а это в перспективе польза и для программирования, и для "стандартной" математики.

Аноним Суб 26 Апр 2014 18:52:59  #57 №347899 

>>347770
Ты ведь траль? Нельзя быть таким тупым. Гомотопия — это базовое понятие топологии. http://en.wikipedia.org/wiki/Topology#Applications_of_topology
>>347774
>(Mu . unMu) -- локальный костыль
Какой костыль? Это handmade изорекурсивный тип. Мне известны только две альтернативы: эквирекурсивные типы, делающие проверку типов неразрешимой, и петушение.
>порой используются неразумно
А порой без их использования у тебя все абстракции посыпятся.
>>347839
>"теория струн"
Ты не знаешь, полезна она или нет. Так было со многими науками вначале. Многие даже были ложны, как алхимия, например, но она дала начало химии, а ее пользу ты отрицать не станешь.
>"теория языков программирования"
NASA пишет на верифицированном диалекте си. Нет PLT — нет верификации, привет Therac-25 и прочее веселье. Тебе конечно и твоего портвешка хватает, и дальнейшее развитие науки кажется тебе избыточным, но это только потому, что ты такая безнадежная манька.
>вещь сама по себе.
"В себе", дебил.
>>347874
>и ещё есть прекрасные языки с зависимыми типами, использующие HoTT
Ломающие новости. Пока вся академическая элита бьется над генерализацией 2D теории типов, залетный петушок из /pr уже видел языки, использующие всю мощь HoTT.
>Ну ничего, это все вопрос времени, ФП уже повсюду, скоро и тайпклассы подтянутся, а через лет 10, "что такое монада?" - будет стандартным вопросом на собеседовании, хочешь ты того или нет, слесарь.
Хоть и наивно звучит, но на самом деле действительно есть некоторая вероятность такого развития событий. Тайпклассы обеспечивают модульность и легки для понимания (это если без зиллиона расширений), а монада — такая же абстракция, как фабрика. В общем-то надо только шершавую монаду-масив генерализовать.

Аноним Суб 26 Апр 2014 19:24:33  #58 №347907 

Computer Science - это Культ Карго
нормальны люди придумали копьютеры а обычные наследственные дебилы придумали культ, написал святые книги (SICP), придумали ритуальные "языки программирования" (scheme, haskell) имеющие сугубо ритуальное значение
Вербуют новых членов и продолжают свои ритуалы в надежде постичь принципиальное непостижимое для них ввиду генетического деффекта

Аноним Суб 26 Апр 2014 19:26:26  #59 №347908 

>>347782>>347894
Ты, конечно, скажешь, что пруф ассистанты нахуй никому не впёрлись. Но они могут быть очень полезны, к примеру, для верификации софта. Некоторые компании теряют миллионы/миллиарды из-за нелепых ошибок.

>>347899
> > (Mu . unMu) -- локальный костыль
> Какой костыль? Это handmade изорекурсивный тип.
Знаю я, речь была о том, что это не сравнимо с апкастом/даункастом из ООП.
> > порой используются неразумно
> А порой без их использования у тебя все абстракции посыпятся.
Не спорю.

Аноним Суб 26 Апр 2014 19:30:22  #60 №347910 

научноюлядки нашли себе новую утопическую идею под гранты
1я- научить дебилов програмировать
и
2я- P=NP
с треском провалились

Аноним Суб 26 Апр 2014 19:34:26  #61 №347911 

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

Аноним Суб 26 Апр 2014 19:56:12  #62 №347915 

>>347907
2 чая, просто 2 чая за мой счет.

Аноним Суб 26 Апр 2014 20:00:57  #63 №347919 

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

Аноним Суб 26 Апр 2014 20:07:16  #64 №347921 

а кто будет проверять ошибки в программе для прув ассистанта?
стратегию то он сам проверит а начальные условия?
требуемое поведение программы нельзя записать одной формулой, это будет целая книга по обьему сравнимая с кодом самой проверяемой программы, кто будет ошибки проверять?

Аноним Суб 26 Апр 2014 20:14:33  #65 №347923 

>>347921
Да никто. Ассистент - он на то и ассистент. Действительно карго-культ, ща как мы все перейдем на хаскель, и все будет заебись. Это 2008. Сейчас 2014, хаскель надежд не оправдал, уже пошло совсем академическое говно.
При этом хуй, пиздящий на бордах об экстремальной эффективности своего языка, никогда не вложится в разработку на этом языке, предпочитая работать на питоне на того, кто вложился в питон. Потому что даже такому хую понятно, что реальной эффективности нет и бабло тупо сольется.

Аноним Суб 26 Апр 2014 20:26:14  #66 №347926 

>>347899
>Ты не знаешь, полезна она или нет. Так было со многими науками вначале
Науки фальсифицируемы, теория струн нет. Она вредна, вредна примерно так же, как рассуждения вокруг птолемеевских эпициклов в Средневековье. Зашли на территорию, для которой не хватает мозгов и рисуют хрустальные сферы, тфу, струны. Понял аналогию? Все эти бесконечные циклы превращаются во что-то очень простое при смене системы координат, но до этого додумывались пару тысяч лет.
Вред банальный - тысячи лучших мозгов планеты страдают схоластической хуйней и кивают на успехи фундаментальных наук типа ОТО, хотя там никакой схоластики не было. Смотрите, у меня диффур похож на уравнение струны, видимо БОГ на что-то этим говорит!! И полвека хуиты на деньги налогоплательщиков.
>NASA пишет на верифицированном диалекте си.
NASA пишет на си с гайдлайнами.
>"В себе", дебил.
Нет, если бы я написал "вещь в себе" (вполне конкретный философский термин), я был бы не прав, как ебанько-журналисты или ты, вторящий за ними. Я имел в виду то, что написал. Хуй саси в общем.

Аноним Суб 26 Апр 2014 20:27:59  #67 №347927 
1398529679090.jpg

>>347899
>Гомотопия — это базовое понятие топологии.
Таки вижу ты сумел накукарекать нужную статью, лол. Удивительно, что такой даун как ты смог это сделать. Хотя о чем это я, гуглотранслейт нынче творит чудеса, да.

Ну ладно, школьник, поясняю тебе по хардкору: сегодня, с теорией топологий имеют дело только кучка продвинутых математиков, решающих по-настоящему узкие задачи, из физики/математики/биологии и никак более, за исключением маленькой группы любителей-даунов, показательно фанящихся под коксик по всяким подобным разработкам;
ну и касательно студентяшек - если они не математики, на замену вышеописанным спецам - теория гопотопий лол нахуй не сдалась и в данный момент существенно бесполезное с практической точки зрения знание.

Рекомендую тебе еще раз там обосраться и кукарекнуть в след, ибо очевидно правду опровергнуть ты едва ли сможешь, лоли лол. :3

>>347907
Двощую.

Аноним Суб 26 Апр 2014 20:44:45  #68 №347935 

>>347907
мартышка_и_очки.txt

Аноним Суб 26 Апр 2014 21:08:48  #69 №347949 

Ладно, я покидаю этот троллекоастер во главе с призраком КК. Оставлю только напоследок: NASA Formal Methods: 4th International Symposium. Тут тебе и кок, и агда, и весь академический инструментарий.
А вдруг это не троллекоастер? Вдруг они серьезно считают формальную верификацию бесполезной? Вопреки тому, что в Coq-Club постоянно появляются новые вакансии, сам Coq уже монструознее C++ (если не говорить о ядре, конечно, CIC — простая и исследованная вещь), тому, что его используют в NASA, да и просто здравому смыслу. Верификация не гарантирует, что программа поведет себя неожиданным образом, но она критически уменьшает вероятность этого. Ладно впрочем, нельзя ожидать от портвешковой маньки понимания чего-либо, что не приближает ее к получению дозы любимого напитка.

Аноним Суб 26 Апр 2014 21:10:28  #70 №347951 

>>347949
>не поведет себя

Аноним Суб 26 Апр 2014 22:11:39  #71 №347996 

>>347949
Ты занимаешься подтасовкой фактов а-ля "квиксорт в одну строчку", который не квиксорт, и жрет память как не в себя. Ты что писал? "NASA пишет на верифицированном диалекте си.". Это - вранье, потому что сишка там обыкновенная, смахивающая на фортран запретом рекурсии и некоторых других вещей. Тестируется оно жестко, в том числе статическим и динамическим анализом, но код все равно пишется вручную, без генерации "sql из хуй пойми чего, но все равно круто звучит". И в качестве доказательств своих слов ты приводишь конференцию, в которой Coq упоминается в докладе двух французов этот Coq форсящих и вакансии математиков. Молодец, хули. 2013 - на хаскетроллинг никто не ведется, выучу очередную хуиту и буду форсить ее.

!!zunHIrSt Суб 26 Апр 2014 22:36:07  #72 №348001 

>>347996
Лень читать тред, но насчёт
> "квиксорт в одну строчку", который не квиксорт, и жрет память как не в себя
предлагаю заглянуть хотя бы в википедию:
https://en.wikipedia.org/wiki/Quicksort#Algorithm
В образовательных целях наивный вариант подходит лучше, потому что удивительно прост и сохраняет все существенные свойства алгоритма. Уже после их разбора нужно обратить внимание на дополнительную память и быстренько рассмотреть in-place вариант.

Аноним Суб 26 Апр 2014 23:19:21  #73 №348010 

>>347949
> Верификация не гарантирует, что программа не поведет себя неожиданным образом
С этого места по-подробнее.

!!zunHIrSt Суб 26 Апр 2014 23:37:19  #74 №348015 

>>348010
Как минимум:
- логические ошибки, не противоречащие спецификации
- сбои в железе
Точность спецификации - штука тонкая. Например, есть

twice n = n * 2

В спецификации можно написать, что функция принимает число и возвращает число. Но тогда можно написать неправильную реализацию, которая, хоть и будет возвращать число, но не n * 2, а, например, n + 1. И это не будет противоречить спецификации. А можно оную максимально уточнить, и написать, что функция должна возвращать число, вдвое большее аргумента. Но тогда спецификация оказывается эквивалентной реализации. На игрушечном примере это ладно, а вот для большой системы в таком случае сам смысл спецификации теряется, потому что когда она становится эквивалентной реализации, появляется необходимость в спецификации-2 над спецификацией-1 и соответствующей верификации и мы возвращаемся к исходной задаче. Потому хорошая, имеющая смысл, спецификация должна нащупывать значимые абстрактные свойства, и ими сужать рамки возможностей неправильных реализаций, оставаясь при этом гораздо компактнее и высокоуровнее реализации.
Аноним Суб 26 Апр 2014 23:48:21  #75 №348018 

>>347996
>Это - вранье
Это не вранье, я просто не могу найти линк. Буквально несколько дней назад читал. Они используют и обычный си и верифицированный.
>но код все равно пишется вручную
А вот это вранье. Вбей "code generation" в книге, на которую я ссылался.
>И в качестве доказательств своих слов ты приводишь конференцию, в которой Coq упоминается в докладе двух французов этот Coq форсящих и вакансии математиков.
Во-первых речь шла о формальной верификации вообще, а во-вторых там не только Coq, но еще и NuSMV, Prover и возможно еще какие-то. А в третьей части того же симпозиума была еще агда. Ты думаешь, они на си что-то там "верифицируют"?
>>348010
Верификация гарантирует (если прувер консистентный, в чем нельзя быть полностью уверенным, но можно быть уверенным больше, чем в простыне на очередном алголе), что все доказанные теоремы верны, но она не гарантирует, что ты выразил этими теоремами именно те свойства, которые подразумевал.

sageАноним Вск 27 Апр 2014 00:02:32  #76 №348025 

>>348015
иди нахуй дебил

Аноним Вск 27 Апр 2014 03:03:45  #77 №348074 

Да никто и не говорит, что верификация исключает все ошибки.
Это просто спецификация более высокого уровня, её проще сформулировать (нужно указать желаемые свойства, а не вычисление, которое их реализует).

>>347949
> сам Coq уже монструознее C++
По количеству, но не по качеству. Coq -- простой и логичный инструмент. Там много разных фич, которые трудно все вместе запомнить, но это и не необходимо.
В отличие от C++.

Аноним Вск 27 Апр 2014 03:04:44  #78 №348076 

>>348018
>Это не вранье, я просто
заврался и обосрался, как у вас, хаскельдебилов, принято.
Это ничего, какой с вас, убогих, спрос.

Аноним Вск 27 Апр 2014 03:23:05  #79 №348085 

>>348074
>Coq -- простой и логичный инструмент.
Это ты про нетипизированный Ltac и километры вырвиглазнейшего кода, написанные на нем? Про сабтайпинг и неявное приведение типов? Про ебаный ад с зависимыми типами? Про возможность определять синтаксис для чего-либо, рискуя при этом перекрыть какую-нибудь из стандартных операций? |- лтаковскую, например. Матчить по этому синтаксису тоже нельзя. Про захардкорженные аксиомы в некоторых тактиках?

Аноним Вск 27 Апр 2014 03:42:19  #80 №348091 
1398555739630.png

>>347949
>Coq

Аноним Вск 27 Апр 2014 06:00:41  #81 №348099 

пруф ассистанты нужны для проверки правильности научных теорий
причем ниписать теорию на традиционном языке математики проще чем на языке пруф ассистанта, зато пруф ассистант может проверить правилольность рассуждений
никакой помощи в доказательствах он не дает- только проверку
естествеено раз никто не доказывает правильность программ с появление пруф ассистантов никто этим темболее не будет заниматся
-
и не надо тут расказывать сказки про некий "верифицироанный C" из НАСА
просто вы (обычные наследственные дебилы) хотите писать на своем прувере для каждой программы не непонятной хуетени и всех убедить что ето значительно повышает надежность но ето всего лиш религиозное действие навроде опрыскивания святой водой

!!zunHIrSt Вск 27 Апр 2014 12:07:04  #82 №348122 

>>348099
> никакой помощи в доказательствах он не дает- только проверку
Такой старый, а про тактики не знаешь.

!CEREBellUM Вск 27 Апр 2014 12:28:31  #83 №348128 

>>348122
в доказательствах записанных для людей такие "тактики" подразумиваются что не каждый человек поймет
для машины доказательства приходится записывать подробнее поскольку "тактики" не дотягивают до понимания человека-математика

Аноним Вск 27 Апр 2014 13:13:13  #84 №348136 

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

Аноним Вск 27 Апр 2014 13:34:32  #85 №348137 

>>347949
90% этой убогой доски - обычные работяги, типа трактористов, пролетариат современного мира, у которого одна идея - получить зарплату за прошлый месяц. Маргиналы, working scum. Перед кем ты распинаешься, няша.

Аноним Вск 27 Апр 2014 13:42:57  #86 №348140 

вобщето КК - крупнейший специалист по искуственному интеллекту в России!

Аноним Вск 27 Апр 2014 13:50:45  #87 №348144 

>>348140
>КК
Это кто? КудКудах?

>по искуственному интеллекту в России
>искуственному интеллекту
Проиграл.

>>348137
Лучшая самоидентификация за все время, что я видел. Самотралль высшего лвла.

Аноним Вск 27 Апр 2014 14:12:38  #88 №348147 
1398593558840.jpg

>>348144
каталог-кун
>Проиграл.
пик

Аноним Вск 27 Апр 2014 14:14:58  #89 №348148 

>>348147
>этот фотошоп
Ясно.

Аноним Вск 27 Апр 2014 14:21:08  #90 №348152 

>>348148
http://planetwars.aichallenge.org/rankings.php

Аноним Вск 27 Апр 2014 14:37:40  #91 №348157 
1398595060871.jpg

>>348147
>каталог-кун
А в чем суть конкурса там была? Почему каталог-кун обосрался?
Какую пользую привнес конкурс в наработки по ИИ?

Аноним Вск 27 Апр 2014 14:52:15  #92 №348159 

>>348140
Он же натуральный даун. Там была олимпиада среди 11-летних?

>>348144
>Лучшая самоидентификация
Вовсе нет, я к этим 90% не отношусь.

Аноним Вск 27 Апр 2014 15:01:04  #93 №348163 

>>348159
>Он же натуральный даун.
Почему?

Аноним Вск 27 Апр 2014 15:04:53  #94 №348164 

>>348163
Если для тебя это не очевидно, ты либо ньюфаг, либо тролль, либо тоже даун.

Аноним Вск 27 Апр 2014 15:10:39  #95 №348167 

>>348164
Но ты например тоже очевидно даун. Где ты не прав?
Так почему он даун? Не смог выйграть конкурс, или что?

Аноним Вск 27 Апр 2014 17:09:12  #96 №348205 

>>348018
Да, соответствие выданных заказчиком теорем подразумеваемым заказчиком свойствам доказать в общем случае невозможно, но это не значит, что не надо доказывать соответствие программы выданным им теоремам. Да, в случае с приложением для 2ch.hk под Android максимум, что ты можешь сделать — это вывести окошко, в котором кратенько описать, что это приложение будет отправлять в интернет только то, что ты вбил в поле «Пост»; но пользователь будет крайне недоволен, если вместе с содержимым этого поля Абулику отправятся все твои пароли. А в случаях, когда заказчик — инженер, разрабатывающий критичную аппаратуру, эти теоремы многократно проверяются или вообще копируются из ГОСТ и ISO.

Аноним Вск 27 Апр 2014 17:13:23  #97 №348210 

я не понял че ты там боромиш но знаю точна чта:

пруф ассистанты нужны для проверки правильности научных теорий
причем ниписать теорию на традиционном языке математики проще чем на языке пруф ассистанта, зато пруф ассистант может проверить правилольность рассуждений
никакой помощи в доказательствах он не дает- только проверку
естествеено раз никто не доказывает правильность программ с появление пруф ассистантов никто этим темболее не будет заниматся
-
и не надо тут расказывать сказки про некий "верифицироанный C" из НАСА
просто вы (обычные наследственные дебилы) хотите писать на своем прувере для каждой программы не непонятной хуетени и всех убедить что ето значительно повышает надежность но ето всего лиш религиозное действие навроде опрыскивания святой водой

Аноним Вск 27 Апр 2014 17:23:10  #98 №348212 

>>348018
> Они используют и обычный си и верифицированный.
А не помнишь, какой? Уж не compsert ли случайно?

И что за книга? В твоём посте нашёл только упоминание конфочки: http://shemesh.larc.nasa.gov/nfm2012/

>>348085
> Это ты про нетипизированный Ltac и километры вырвиглазнейшего кода, написанные на нем?
Ну это же проблема тех, кто этот код написал. Ну то, что на Qed у нас может быть отвергнут пруф-терм, тоже не айс, конечно. Но в принципе ты и не обязан пилить собственные тактики.

> Про сабтайпинг и неявное приведение типов?
Про это можешь поподробнее?

> Про ебаный ад с зависимыми типами?
Ты про зависимый паттерн матчинг? Согласен, уёбищно сделано. В агде вроде лучше. Мне приходится определять такие термы тактиками.

> Про возможность определять синтаксис для чего-либо, рискуя при этом перекрыть какую-нибудь из стандартных операций? |- лтаковскую, например.
Покажи, когда это проблема.

> Матчить по этому синтаксису тоже нельзя.
Поясни, пожалуйста.

> Про захардкорженные аксиомы в некоторых тактиках?
А разве это проблема? Ну не используй такие тактики.
По-моему вопрос использования таких тактик эквивалентен использованию некоторых аксиом.

Аноним Вск 27 Апр 2014 17:23:26  #99 №348213 

>>348205
ты тут пытаешся сказать что какоето требование ГОСТ или ISO по безопасности программы можно выразить в пруфАсистанте и доказать что заданная конкретная программа ему соответствует?
сперва приведи хоть 1н пример такого доказательства

Аноним Вск 27 Апр 2014 17:26:24  #100 №348214 

>>348163
Смотри его видос на ютабе, где он ищет невесту.

Аноним Вск 27 Апр 2014 17:49:34  #101 №348217 

>>348212
>А не помнишь, какой? Уж не compsert ли случайно?
Помнил бы, нашел бы и линк. Про CompCert гуглил, но не нашел.
>И что за книга? В твоём посте нашёл только упоминание конфочки
На гуглкнигах вся эта конфочка лежит одним файлом, так что назвал книгой.
>Ну это же проблема тех, кто этот код написал.
Это проблема Ltac, на котором невозможно написать что-нибудь стройное.
>Про это можешь поподробнее?
Я не знаток, посмотри здесь: http://coq.inria.fr/refman/Reference-Manual021.html
>Ты про зависимый паттерн матчинг?
И про немощную унификацию.
>Мне приходится определять такие термы тактиками.
Это стандартная процедура — определять все через refine.
>Покажи, когда это проблема.
В SF (|-) переопределялся, из-за чего я не мог пользоваться лтаком вообще. Может можно было как-нибудь решить с помощью неймспейсов, но я поленился.
>Поясни, пожалуйста.
Задаешь специальный синтаксис для конструкторов какого-нибудь типа, к примеру WHILE b DO e END для WhileExpr b e.
И паттерн-матчинг будет работать по WhileExpr b e, но не по WHILE b DO c END. Правда я давно на коке писал последний раз, не уверен, что так во всех случаях, но в некоторых точно.
>А разве это проблема? Ну не используй такие тактики.
Это как побочные эффекты, только еще хуже. Такие тактики должны быть "завернуты в монаду", чтобы было видно, что они потенциально нарушают консистентность, поскольку даже если они безвредны по отдельности, могут не быть безвредны вместе. Уж хотя бы какие-нибудь конвенции именования были бы.

Аноним Вск 27 Апр 2014 18:04:11  #102 №348221 

>>348217
если ты не осилил Prolog даже не пытайся осилить Coq
у тебя обычный наследственный дебелизм же
ты выучил всю терминалогию и научился составлять выглядищие правильными предложения
все - ето твой потолок, выше головы не прыгнеш


Аноним Вск 27 Апр 2014 21:51:11  #103 №348281 

> Про CompCert гуглил, но не нашел.
Странно, у меня первая ссылка. Он достаточно известный, это проект Xavier Leroy.
http://compcert.inria.fr/

> На гуглкнигах вся эта конфочка лежит одним файлом, так что назвал книгой.
Ок, нашёл теперь.

> Это проблема Ltac, на котором невозможно написать что-нибудь стройное.
Ладно, возможно. Я сам пока не писал свои тактики; но вот Chlipala в своём CPDT не очень вырвиглазно использует.

> сабтайпинг и неявное приведение типов
Видимо, с этим чаще сталкиваются те, кто формализует математику на Coq. Я не пользовался этими штуками.

> > Ты про зависимый паттерн матчинг?
> И про немощную унификацию.
А что с ней не так? Я сталкивался только с проблемами при паттерн-мэтчинге, когда уже известная информация не распространяется дальше по терму и приходится использовать анальные трюки вроде оборачивания в лямбду веток матча.
Паттерн-мэтчинг вообще меня сильно раздражает в Coq.

> В SF (|-) переопределялся, из-за чего я не мог пользоваться лтаком вообще. Может можно было как-нибудь решить с помощью неймспейсов, но я поленился.
Ну это всё-таки "сам себе злобный буратино". Хотя заранее предусмотреть всё-таки трудно бывает.
Меня из нотаций больше бесит то, что * и + конфликтуют часто (для чисел и типов).

> И паттерн-матчинг будет работать по WhileExpr b e, но не по WHILE b DO c END.
Не знал. Странно как-то, что так сделали.

> > А разве это проблема? Ну не используй такие тактики.
> Это как побочные эффекты, только еще хуже.
Ну в принципе точно такая же проблема будет с теоремами, доказанными с помощью какой-то аксиомы. Про монаду согласен. Просто это проблема не тактик, а вообще использоования аксиом.

Аноним Вск 27 Апр 2014 21:52:14  #104 №348282 

>>348221
А при чём тут Prolog?

Аноним Вск 27 Апр 2014 23:21:05  #105 №348318 

>>348213
Да. Есть, например, ГОСТ 24.104-85. Из него и берутся дифуры для конкретных АСУ. Ведь это так делается, да? Сейчас, открою, приведу пример дифура. ЕБТВОЮМА~

Аноним Пнд 28 Апр 2014 00:33:38  #106 №348333 
[url]

>>348214
Сука, я люто проиграл.

Аноним Пнд 28 Апр 2014 00:37:42  #107 №348334 

>>348333
Бляяя, я аж под себя проиграл с этого
>давай девочек от 15 до 18
сука блядь, охуеть просто

Аноним Пнд 28 Апр 2014 00:58:31  #108 №348343 

>>348281
>Странно, у меня первая ссылка. Он достаточно известный, это проект Xavier Leroy.
Да нет, про CompCert я знаю, не нашел его причастности к NASA.
>не очень вырвиглазно использует.
Использовать их удобно, но ты на код посмотри: http://adam.chlipala.net/cpdt/repo/file/e0c5b91e2968/src/CpdtTactics.v
И это Adam Chipala, а не какой-то хуй собачий. В SF вообще кишки. Просто Ltac уродлив. В идрисе тактики завернуты в монаду и все выглядит благопристойно, хотя я особо не возился.
>А что с ней не так?
Поиграйся с агдой, разница будет очевидна.
>Не знал. Странно как-то, что так сделали.
Я кажется вспомнил. По WHILE b DO c END можно матчить, если все выражения являются переменными, которые прямиком транслируются в конструктор. То есть если надо WhileExpr b c. А если у тебя WhileExpr b c = WHILE b && b DO c END, тогда матчить по правой части нельзя нельзя.
>Ну в принципе точно такая же проблема будет с теоремами, доказанными с помощью какой-то аксиомы.
Да, но аксиомы вводятся более сознательно, хотя и тут возможны аналогичные ситуации.

Аноним Пнд 28 Апр 2014 01:24:25  #109 №348349 

>>347910
Но ведь пол борды тут доказывает, что первое получилось.

Аноним Пнд 28 Апр 2014 03:21:42  #110 №348365 
[url]

Официальная музыкальная группа хаскеллача

Аноним Пнд 28 Апр 2014 05:55:23  #111 №348372 

>>348349
в каком месте получилось?
это тред полон страданий обычных наследственных дебилов находящихся в поиске интсрумента на котором они смогут программировать
но пока их высшее достижение - знание терминологии и научноподобные расуждения

Аноним Пнд 28 Апр 2014 05:57:28  #112 №348373 

>>348318
ну записал ты дифур, как доказывать будеш?

Аноним Пнд 28 Апр 2014 06:01:13  #113 №348374 

>>348282
COQ ето Prolog с стратегиями

Аноним Пнд 28 Апр 2014 06:21:17  #114 №348377 

>>348372
Научноподобных рассуждений не было.

Аноним Пнд 28 Апр 2014 06:23:36  #115 №348378 

>>348374
Лолшто?

Аноним Пнд 28 Апр 2014 09:26:32  #116 №348394 

>>348373
В Axiom же.

Аноним Пнд 28 Апр 2014 10:59:06  #117 №348409 

>>348343
Всё-таки эти проёбы, в основном, не выстрелы себе в ногу, как в C++, где у тебя из-за косяков может течь память и т.п.

Аноним Пнд 28 Апр 2014 11:22:12  #118 №348412 

>>348409
данет все заебися, просто ответ неправильный получится.
но наша цель не ответы получать а создавать видимость дейтельности

Аноним Пнд 28 Апр 2014 11:40:56  #119 №348414 

>>347605
>>347612
>>347615
>>347672
>>347680
Уберплебеи.

>>347682
Двачую. Гомологии и когомологии чертовски сексуальны. А когда вся эта топлогическая няшнота сливается с матлогикой в лице типов -- ваще кайф.

347700
Что именно ты подразумеваешь под "теорией множеств"? Если классику, ZFC, то никогда, ибо неконструктивна. Но есть ещё тысячи способов закодировать множества и коги в них вполне могут.

>>347727
Ну вообще-то каты и выросли из топологии и сама топология - это не геометрия с убранным растоянием, так говорить слишком грубо. Это касается разве что только многообразий. А, например, нехаусдорфовы пространства никак не тянут под такое определение.
И мне не нравится слишкой размытый переход от катов к ООП. На мой взгляд, его нет. Точнее, его, конечно, можно построить достаточно легко, ибо аксиомы катов предельно упрощены и под них можно положить всё, что угодно. Но ООП всё-таки не сказать что блестяще формализовано и цели такой не было, ООП -- это защита от дурака, чисто прикладная фишка для (по мнению некоторых) читаемости кода.
Совсем другая история с ФЯП. Тут уже применение катов очевидно, потому что Лямбда-Калкулус является cartesian closed category.

347737
Ну или ZFC с конструктивными приблудами.

347743
Или, может быть, он программист (=слесарь), а хаскеллист уже больше прикладной математик. Хотя всё равно, любой, кто ещё кодит -- далёк от просветления. И это логично, чем выше квалификация программиста, тем меньше он пишет строчек кода в день. Точная нижняя грань -- не писать код вообще.

>>347770
> Ни одной строчки о реально полезном практическом применении.
У гомотопий-то? Пиздец. А ты прям ждал там раздела "практическое применение"? Вот же плебей. Погугли, сколько теорем в теории чисел (из которой растут ноги криптографии) доказано с помощью методов абстрактной алгебры.

Аноним Пнд 28 Апр 2014 13:00:42  #120 №348438 

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

Аноним Пнд 28 Апр 2014 14:32:34  #121 №348469 
1398681154167.png

>>348414
Ебать тебя порвало. Кончай уже бугуртеть, обосрышь, ты обосрался уже везде где только можно и только ухудшаешь свое положение.

>А ты прям ждал там раздела "практическое применение"?
>Погугли
Проиграл с дауна.

Аноним Пнд 28 Апр 2014 14:47:47  #122 №348472 

>>348469
Я мимокрокодил и первый раз в тред написал, чини детектор.

> Проиграл с дауна.
А что тебе не ясно? Спроси. Может, и такому глупому и агрессивному получится помочь.

sageАноним Пнд 28 Апр 2014 14:50:14  #123 №348475 

>>348414
>Погугли, сколько теорем в теории чисел (из которой растут ноги криптографии) доказано с помощью методов абстрактной алгебры.
При чем тут теоремы и обосрактная алгейбра, защеканец? Ты давай пример практического применения в программе, которая не направлена изначально на расчет математической хуйни.

Аноним Пнд 28 Апр 2014 14:55:31  #124 №348478 

>>348475
Твой уровень понимания математики настолько низок, что тебе нужно только разжёвывать. А у меня желания нет. Если хочешь - напиши конкретный вопрос в вопрос-ответ-тред или математика-тред в наукаче.

Аноним Пнд 28 Апр 2014 15:25:19  #125 №348486 
1398684319347.jpg

>>348472
>>348478
>Ты давай пример практического применения
>напиши конкретный вопрос

Ты ничему не учишься, школьник. Очень жаль.

Аноним Пнд 28 Апр 2014 20:06:07  #126 №348582 

>>348475
Манька, сядь уже обратно за свой кубикл.

sageАноним Пнд 28 Апр 2014 20:28:46  #127 №348600 

> практическое приминение, real world
ненавижу таких

sageАноним Пнд 28 Апр 2014 20:29:53  #128 №348601 

>>348600
вернее, презираю

Аноним Пнд 28 Апр 2014 22:41:16  #129 №348689 

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

Аноним Пнд 28 Апр 2014 22:45:30  #130 №348694 

>>348689
тему кандидатской назови для начала

sageАноним Пнд 28 Апр 2014 22:49:59  #131 №348697 

>>348694
прикладная полемика с приложениями к имиджбордам

!!zunHIrSt Пнд 28 Апр 2014 23:43:23  #132 №348732 

>>348689
В твоей жизни есть важные вещи, которые имеют для тебя большое значение. Это относится и к большинству твоих действий. У меня — все иначе. Для меня больше нет ничего важного — ни вещей, ни событий, ни людей, ни явлений, ни действий — ничего. Но все-таки я продолжаю жить, потому что обладаю волей. Эта воля закалена всей моей жизнью и в результате стала целостной и совершенной. И теперь для меня не важно, имеет что-то значение или нет. Глупость моей жизни контролируется волей. Я научился видеть, и говорю, что нет ничего, что имело бы значение. Теперь — твоя очередь. Вполне вероятно, что в один прекрасный день ты научишься видеть, и тогда сам узнаешь, что имеет значение, а что — нет. Для меня нет ничего, имеющего значение, но для тебя, возможно, значительным будет все. Сейчас ты должен понять: человек знания живет действием, а не мыслью о действии. Он выбирает путь сердца и следует по этому пути. Когда он смотрит, он радуется и смеется; когда он видит, он знает. Он знает, что жизнь его закончится очень скоро: он знает, что он, как любой другой, не идет никуда: и он знает, что все равнозначно. У него нет ни чести, ни достоинства, ни семьи, ни имени, ни родины. Есть только жизнь, которую нужно прожить. В таких условиях контролируемая глупость — единственное, что может связывать его с ближними. Поэтому он действует, потеет и отдувается. И взглянув на него, любой увидит обычного человека, живущего так же, как все. Разница лишь в том, что глупость его жизни находится под контролем. Ничто не имеет особого значения, поэтому человек знания просто выбирает какой-то поступок и совершает его. Но совершает так, словно это имеет значение. Контролируемая глупость заставляет его говорить, что его действия очень важны, и поступать соответственно. В то же время он прекрасно понимает, что все это не имеет значения. Так что, прекращая действовать, человек знания возвращается в состояние покоя и равновесия. Хорошим было его действие или плохим, удалось ли его завершить — до этого ему нет никакого дела.

Аноним Втр 29 Апр 2014 00:34:16  #133 №348748 

>>348091
http://coq.inria.fr/

sageАноним Втр 29 Апр 2014 01:07:20  #134 №348756 
[url]

пусть

sageАноним Втр 29 Апр 2014 10:18:02  #135 №348796 
[url]

>>348756
а он файный)

Аноним Втр 29 Апр 2014 11:53:32  #136 №348839 

>>348756
Я думаю, когда он про друга рассказывал, он на самом деле себя имел ввиду. А то был один знакомый, который чисто случайно как и я занимался топологией, чисто случайно упарывал, и чисто случайно делился со мной какие там вопросы он кому задаёт во время трипа. Ну-ну. http://lurkmore.to/%D0%A3_%D0%BC%D0%BE%D0%B5%D0%B9_%D0%BF%D0%BE%D0%B4%D1%80%D1%83%D0%B3%D0%B8_%D1%81_%D0%B5%D1%91_%D0%BF%D0%B0%D1%80%D0%BD%D0%B5%D0%BC

sageАноним Втр 29 Апр 2014 12:12:43  #137 №348847 
1398759163471.jpg

>>348839
думаешь он торч?

Аноним Втр 29 Апр 2014 13:30:21  #138 №348892 

>>348694
Я не он, но могу назвать своё направление -- адаптивные методы идентификации нелинейных систем с применением нечёткой логики.

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

Аноним Втр 29 Апр 2014 14:00:24  #139 №348901 

>>348892
>адаптивные методы идентификации нелинейных систем с применением нечёткой логики.
Математика уровн пр

Аноним Втр 29 Апр 2014 14:03:57  #140 №348903 

>>348901
Какие проблемы?

Аноним Втр 29 Апр 2014 14:09:54  #141 №348904 

>>348847
Он же говорил, в молодости вёл неправильный образ жизни, упарывал психоту, сейчас видимо завязал, занимается топологией, танцует, жонглирует. Ну может скушает марочку, чтобы разобраться в особо сложной теореме, но не больше.

Аноним Втр 29 Апр 2014 14:25:18  #142 №348908 

Эй, элита!

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

Итак, байтоёбы. Я примерно представляю, от чего они получают удовольствие. Написать работающий сокет, получить прямой доступ к железу - это очень увлекательно. Да, изобретатели велосипедов никому не нужны, но они по-своему счастливы, когда они с красными глазами после бессонной ночи смогли-таки вручную написать программу, передающую запрос серверу на скорости 8 кб/c.

Энтерпрайзо-макаки. Пишут то, что им сказали, работают 8 часов в сутки. Вроде бы и деньги есть, и делают что-то полезное, но писать код по одинаковым шаблонам, используя всё готовое - ужасно скучное занятие. Получать удовольствие, если ты пишешь шаблонный код, невозможно.

Функциональщики. А от чего они получают удовольствие? Что приносит интерес? Поясните.

Аноним Втр 29 Апр 2014 14:41:20  #143 №348917 
1398768080854.png

>>348908
>Функциональщики. А от чего они получают удовольствие? Что приносит интерес? Поясните.
Даже лень объяснять. Почитай
http://newstar.rinet.ru/~goga/sicp/sicp.pdf

Аноним Втр 29 Апр 2014 14:58:45  #144 №348926 

>>348908
>Скажите, а как вы получаете удовольствие от программирования?
От программирования - да.
>Допустим
Не допустим. Любые практические задачи (как написание низкоуровневого кода, так и энтерпрайз и гейдев) могут решаться как и императивном говне, так и на функциональных языках. Когда ты пишешь какой-нибудь загрузчик спредшитов для энтерпрайза на джаве - это жопаболь, такое чувство, что в языке всё сделано против тебя, чтобы заставить тебя заниматься хуйнёй, запутывать и размазывать задачу тонким слоем говна по рассыпухе классов. На Хаскеле наоборот всё направлено на удобство. Т.е. решая одну и ту же задачу в одном случае ты страдаешь и проклинаешь жавамакак, в другом случае наоборот думаешь, какие молодцы, охуенно сделали.

Аноним Втр 29 Апр 2014 15:08:25  #145 №348928 

>>348908
В общем, даже лень тебе что-то объяснять.
Таких, как ты — миллионы, серых и отвратительных, как плевки на асфальте. Приходящих сюда ежедневно с ведром грязной воды, которой мыли полы, вместо мыслей.
Вам все уже было сказано и не раз, поэтому и встречают тебя пастой, апатией и струей урины.

Аноним Втр 29 Апр 2014 15:43:27  #146 №348944 

>>348926
> Т.е. решая одну и ту же задачу в одном случае ты страдаешь и проклинаешь жавамакак, в другом случае ты страдаешь и проклинаешь трансформеры монад.
Поправил, не благодари

Аноним Втр 29 Апр 2014 16:16:13  #147 №348965 

>>348944
>трансформеры монад
паста_про_то_как_кучер_яшка_начитался_господских_разговоров_и_начал_выкладывать_их_из_кусочков_говна_не_понимая_смысла_слов.txt

Давай начнём с того, что при разработке на Хаскеле вообще не приходится писать собственные трансформеры. Того что есть transformers, mtl и monad-control хватает для любой практической задачи. Максимум - уже готовый трансформер заворачивается в newtype и всё что надо наследуется через generalized newtype deriving. Потому что сделано для людей. Ну да, быдло трансформеров очень боится, потому что не понимает как они работают. Назови последний трансформер, который тебе пришлось писать руками самому? Вооот. Обтекай.

Аноним Втр 29 Апр 2014 16:55:25  #148 №348979 

>>348965
Как будто с готовыми трансформерами не приходится жрать говно с lift $ do

Аноним Втр 29 Апр 2014 17:14:23  #149 №348996 

>>348979
Не приходится, дибил. Потому что возможны 2 варианта: либо подразумевается, что базовая монада будет использоваться в приложении, тогда она просто наследуется, либо подразумевается, что будет использован ограниченный интерфейс, тогда этот интерфейс создаётся и в нем действительно есть ручной лифтинг, но только в реализации этого интерфейса, сам он в приложении используется как есть, без всяких lift. Короче, либо выучи Хаскель, либо уябывай нахуй, потому что твои охуенные истории заебали уже.

Аноним Втр 29 Апр 2014 17:17:09  #150 №348999 

>>348996
Только не бейся в истерике, прошу.

Аноним Втр 29 Апр 2014 17:35:25  #151 №349013 

>>348999
В какой еще истерике, долбоёб? Я спокоен как удав. Ты правда думаешь, если бы твой долбоебизм и правда мог бы вызвать у кого-нибудь истерику, его бы уже давно на скорой увезли, потому что ты тут годами хуйню постишь, вместо того, чтобы чему-нибудь научиться. Необучаемость неизлечима, хуле.

Аноним Втр 29 Апр 2014 17:41:00  #152 №349020 

>>349013
Сука проиграл с истерички))))
> ты тут годами хуйню постишь, вместо того, чтобы чему-нибудь научиться. Необучаемость неизлечима, хуле.
Прям про тебя

Аноним Втр 29 Апр 2014 17:54:28  #153 №349027 

>>349020
Маньку макают в собственную мочу, а маньке всё божья роса.

sageАноним Втр 29 Апр 2014 19:15:33  #154 №349080 

Типичный тред о математике, подтверждающий генетическую ущербность анонимуса.

Аноним Втр 29 Апр 2014 21:12:54  #155 №349149 

>>348796
А жюри не оценили :( Охуенно же.

Аноним Втр 29 Апр 2014 21:20:33  #156 №349155 

>>348839
Очевидно по-моему же. Тем более, он сразу после телеги про "друга" сказал "вот этим я и занимаюсь последние 15 лет", с чего бы он стал заниматься вещью, которая привидилась его другу во время трипа?

Аноним Втр 29 Апр 2014 21:36:28  #157 №349161 

>>348732
Карлос, залогинься
проебал свой Тональ, проеби другому?

Аноним Втр 29 Апр 2014 23:31:20  #158 №349218 

>>348917
>>348928
Какие же вы функциональщики?

Вы явно ненавидите ФП, оно вам осточертело. Потому что человек, действительно в чём-то заинтересованный и чем-то увлечённый, может об этом говорить постоянно. Я, например, часами могу рассказывать о программировании под Windows и о Direct3D. А вы - просто залётные петушки, желающие показаться элитариями.

sageАноним Срд 30 Апр 2014 04:00:09  #159 №349306 
1398816009056.gif

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

Аноним Срд 30 Апр 2014 08:39:40  #160 №349334 

>>349306
>Я, например, часами могу рассказывать о программировании под Windows и о Direct3D.

sage!A/handsOmE Срд 30 Апр 2014 09:54:02  #161 №349352 
1398837242436.jpg

>>349334
ты всего лишь частный случай
у нас тут тредик о матиматике
так что давай сначала строго определи что есть
> увлечённый
а потом докажи
> человек, действительно в чём-то заинтересованный и чем-то увлечённый, может об этом говорить постоянно

Аноним Срд 30 Апр 2014 13:38:37  #162 №349409 

>>349352
Увлечённый - человек, интересующийся какой-то темой, человек, получающий от неё моральное удовольствие(как от получения новой информации, так и от достижения целей).


Предположим, что человек не может разговаривать постоянно о какой-то теме с собеседником.
Возможны 3 варианта:
1) Собеседник разбирается в теме. В таком случае он может дать новую информацию, а если человеку неинтересна информация о его теме, то получаем, что он темой не увлечён.
2) Собеседник не разбирается в теме, но выражает интерес. Тогда лучше его привлечь к теме, т.к. в будущем он сам сможет стать источником информации. Отсюда получаем снова, что человек темой не увлечен.
3) Собеседник не разбирается в теме и не выражает интерес. Тогда ничего сказать нельзя.

Пост >>348908 отвечал пункту 2). То есть в данном случае ответчики не были увлечены ФП.

Аноним Срд 30 Апр 2014 17:07:01  #163 №349448 

А неслабо так мартыханам припекло. Найс. Молодец ОП, что запостил.

Аноним Срд 30 Апр 2014 17:26:45  #164 №349454 

>>349409
понимаш торагой, все ФП настолько бесполезная весь что рассуждать о ней серьезно могут только обычные наследственные дебилы кторые вообще ничего не знают кроме ФП пропоганды
***
а увликаются ФП от безысходноси, когда наследственный генетический деффект не дает возможности понять архитектуру Фон-Неймана

Аноним Срд 30 Апр 2014 19:10:14  #165 №349482 
1398870614053.jpg

>>349448
А то ж! Я чемпион троллинга ^_^
ОП

comments powered by Disqus

Отзывы и предложения