RS
Опять же чисто под математику. Тьюринг взял уже существовавшие счеты, прицепил на них типы, вычислимость и прочую арифметику и появились компы.
Size: a a a
2019 October 01
RS
Под крипту всякую.
ҪҸ
годный тред)
RS
Ну а дальше уже, можно сказать, современные компы. Первый настоящий компьютер, спрятанный от "освободителей" в подвале, первый высокоуровневый ЯП, первое венчурное финансирование (стартап, лол) от IBM и вот мы щас в телеге сидим, закодированные, Ади Шамир, RSA и прочие штучки, которые помешают Блетчли Парку нас читать.
RS
Как-то так:)
VK
А еще, кмк, на хаскелле не пишут, потому что у него задачи нет. Он как бы не для чего. Любой язык должен быть хоть чуть-чуть domain specific, иначе его ждет печальное будущее.
мне нравится то чем занимался Воеводский - HoTT (homotopy type theory)
RS
мне нравится то чем занимался Воеводский - HoTT (homotopy type theory)
Ну это же достаточно продвинутая тема, сложная математика. Типа доказательные языки и т.п.
RS
В ПМПУ ребята помню чем-то таким занимались.
VK
там и к историческим событиями теория типов подводится и к формализации математических трудов и тд
RS
Ну там прям вообще жесть.
VK
жаль что он в 2017 году ушел из жизни конечно
VK
мог перевернуть мир своими трудами
RS
там и к историческим событиями теория типов подводится и к формализации математических трудов и тд
Да, я че-то слышал про формальные группы, не знаю, это то о чем ты говоришь, или нет, я не специалист.
RS
У меня друг работал по теории чисел, работу писал про спаривание гильберта в этих самых лоренцевых группах.
RS
Жесткий матан.
RS
мне нравится то чем занимался Воеводский - HoTT (homotopy type theory)
А, я перпутал. Я про Востокова подумал, лол. Неуч :)
VK
математические доказательства сложных теорем занимают много томов и мало кто уже их изучает, подвергает сомнению, а Воеводский как раз хотел создать язык для описания всех этих трудов, чтобы формализовать можно было и использовать для дальнейших доказательств и это было бы круто
АО
Ну а дальше уже, можно сказать, современные компы. Первый настоящий компьютер, спрятанный от "освободителей" в подвале, первый высокоуровневый ЯП, первое венчурное финансирование (стартап, лол) от IBM и вот мы щас в телеге сидим, закодированные, Ади Шамир, RSA и прочие штучки, которые помешают Блетчли Парку нас читать.
Вопреки фильму Тьюринг свою машину разрабатывал совершенно для другово. Он хотел доказать логистам что не возможно вывести алгоритм который бы доказал или опроверг другой алгоритм (вычислимость - Halt Problem) и доказал что есть алгоритмы для которых не возможно сказать алгоритмически закончатся (Halt) они когда либо или нет. Тьюринг тупо пытался доказать кому-то что они не правы и все.
RS
Вопреки фильму Тьюринг свою машину разрабатывал совершенно для другово. Он хотел доказать логистам что не возможно вывести алгоритм который бы доказал или опроверг другой алгоритм (вычислимость - Halt Problem) и доказал что есть алгоритмы для которых не возможно сказать алгоритмически закончатся (Halt) они когда либо или нет. Тьюринг тупо пытался доказать кому-то что они не правы и все.
Типа да, это же основная аксиома , что нельзя узнать будет ли 🕒❓когда-нибудь останов той или иной проги
RS
Там еще была тема, что любую вычисляемую рекурсивную функцию можно переписать итеративно, ну если точно известно, что она выполнима. А какой-то чел придумал функцию, которая ГАРАНТИРОВАННО вычисляется, но при этом ее невозможно переписать итеративно. На ней сейчас компайлеры бенчмаркят.