Он создаёт ошибку? Вызывает ошибку? Почему нельзя записать его как
{
"to": "пуэп",
"cmd": "error",
"list": [o8, o16, o8, o8, o16, o16, o16, o8],
"ostr": true
}
и интерпретировать????
Его можно "передать в систему и не беспокоиться о внутренней реализации?" Кажется, кто-то только что изобрёл Observer, Command и Strategy. А может даже и event-based system и хэш-таблицы.
Макросы? Кто-то изобрёл Interpreter и DSL.
Функции как переменные? Указатели на функции были ещё в C.
Лямбды и создание функций на лету, map и т.п.? Давно есть даже в C++.
Рекурсия никуда не пропадала.
Требования писать функции чисто и по возможности использовать иммутабельность - были ещё в учебниках 1980-х.
Из материалов этой книги довольно ясно следует, что однозначное определение доказательства вообще невозможно. Можно говорить только о тавтологических утверждениях, но пользы от них немного (они не увеличивают знание). Ну или о консенсусе математиков по какому-то вопросу.
Ну и вспоминайте получше кандидатский курс - то неужели там не рассказывают, что до конца неясно, на каких аксиомах основана математическая модель ОТО (понятно, что пространство неэвклидово, но как его описать неясно) и что мы не знаем, выполняется ли там, к примеру, аксиома Архимеда? Однако эта нехватка формализации не мешает вести исследования. Есть даже подходы, которые прямо отрицают важность этих оснований.
Невозможно отличить теоремы от не-теорем без доказательства, что утверждение теоремы действительно следует из данного набора аксиом.
То есть великая теорема Ферма до 1995 года не была теоремой? Это новое слово в истории математики.
Из этой заявления следует много не менее странных: например, неясно, как быть с невыводимыми теоремами, которые описываются теоремой Гёделя о неполноте. Их истинность доказать можно, а вывести из аксиом - нельзя.
Если бы вы разбирались в теме, то аргументация звучала бы так:
Scheme и чисто функциональные языки активно применяются в области X. Да, они не подходят для программирования контроллеров, но пример современного использования можно найти в книге Y.
Для примера: вот код, который описывает математическую матрицу средствами Haskell. После того, как вы определили матрицу таким образом, вы можете легко производить над ней операции вот так:
Я допускаю, что вам интересно рассказывать про лемму Йонеды. Но вот что важно: вас про лемму Йонеды и капитализацию криптовалют никто не спрашивал.
Так что я не берусь вам ничего объяснять - потому что мне очевидно, что вы ничего из моих объяснений не поймёте. Вы - гений, вы знаете лемму Йонеды. Нам всем остаётся только внимать такому великому гению, как вы.
Да, который, в свою очередь, используется в куче упомянутых ниже приложений. Чем плохо?
Тем, что gcc используется несколько шире.
А, то есть, теперь какие-то измеримые критерии вам не нужны? Ну понятно.
Заявления каких-то компаний и базворды в их отчётах - так себе аргумент. И тем более их капитализация.
По вашему нет компаний с большей капитализацией, которые используют Visual Basic?
Внутри кодовой базы гитхаба. Вероятно, для этого нужно туда устроиться.
Ну то есть вы предполагаете, что она там есть.
А я предполагаю, что там С++. Или Go. Или Rust. Или Visual Basic. Попробуйте опровергнуть.
У вас аргументы всё мощнее. А я помню, как LLM рекомендовала пользователю пиццу с клеем, или что-то такое. И что теперь это говорит об ООП, с использованием которых по-вашему сделаны LLM?
Это говорит о том, что никакой "защиты от ошибок" в Хаскелле нет. Раз один городской сумасшедший смог её обойти самым примитивным способом.
Как вы сделали этот вывод из моих слов? Или это открытая вами теорема, доказательство которой — ненужная мелочь?
Если вы не знаете, как аргументированно опровергать - попробуйте изучить учебник логики для первого курса.
А то как-то обидно получается - рассуждаете о доказательной теории и алгебре, а аргументировать только помойными червями умеете.
Обратитесь к обезьянкам в зоопарке и к помойным червям. Вы явно эксперт в этой области, они с удовольствием вас послушают. Уверен, вы просто раздавите их вашим космическим интеллектом.
Market cap у какого-нибудь cardano, где это используется — 14 миллиардов, входит в топ-10
А почему не Hamster Combat? У него тоже была большая капитализация.
Или в гитхабе для анализа исходников.
Где я могу увидеть этот анализатор? На каком языке он написан?
Или в фейсбуке антиспам.
Я помню, как фейсбуковский антиспам не мог ничего сделать против одного отморозка, который призывал к убийствам и в каждый комментарий вставлял картинку.
Антиспам гордо рапортовал, что на картинке не обнаружено ничего плохого...
Мощная система. И что, тоже на Scheme написана?
Если вы не смогли прочитать прямо написанное утверждение о том, что возможность категориальной формулировки матриц не означает, что надо обмазываться теоркатом, то определители вам считать ещё рано.
Ну то есть вы не знаете, как считается определитель.
Этому обучают на профильных факультетах. Примерно на первом курсе.
обобщается до потребностей физиков с их физическими теориями (чё-то там про ОТО, струны, суперсимметрии, вот это всё — я в этих приложениях не настолько шарю, чтобы говорить что-то определённое).
Если не шарите - попробуйте восполнить оскорблениями. Расскажите им про помойных червей и обезьянок в зоопарке. Они будут вас внимательно слушать.
Вам стоило бы немного поизучать логику. Аргументация оскорблениями (то у вас обезьянки в зоопарке, то копошение червей у мусорного пакета) - признак небольшого ума.
Думаю, за меня неплохо ответит книжка Имре Лакатоса "Доказательства и опровержения". Там довольно подробно расписана проблема того, как одна тривиальность проваливается в другую.
Поэтому открытие теорем кажется мне более важным, чем их формальное доказательство.
К сожалению, мне нет дела до того, какие слова или выражения вы выучили. Будь то "монада", "эндофунктор", "аорист" или "закозельская кукарямба".
Если бы это было важно - это бы нашло применение где-то за пределами случайных проектов в случайных компаниях и академических исследований о заведении лямбды за сигму.
Пока же это просто до зубной боли нудная реклама, обстрел читателя кучей терминов из крайне узких разделов математики и на каждом шагу при попытке узнать подробности наталкиваешься на то, что привычные термины просто переопределены по своему.
Это применяется для написания компиляторов? Каких компиляторов? Как выясняется, это компиляторы из одного диалекта LISP в другой диалект LISP, описанные в мощнейшем университетском курсе 40-летней давности.
Это позволяет писать программы без ошибок? Как выясняется, под программой понимается не приложение, а кусок кода, который ничего не делает или считает ряд Фибонночи.
Это позволяет писать код яснее и короче? Приведённые примеры - что-то инопланетное, из них вообще невозможно понять, что происходит, как это отлаживать и как поддерживать. Как подсчитать определитель у определённой таким образом матрицы - непонятно. Из лемма Йонеды это никак не следует.
Однако на ООП реализовано множество приложений, которыми мы пользуемся каждый день. В том числе и языковых моделей.
В то время как другие были заняты изучением обезьянок в зоопарке. Возможно, как раз для этой важнейшей задачи Scheme и является крайне востребованным языком.
Удручающе напоминает "великую теория Смысл-Текст" Мельчука и Жолковского. В ABBYY на её основе лет 10 делали систему автоматического перевода - и так и не сделали.
Теорема Пифагора была доказана ещё древними вавилонянами.
Теорема о четырёх красках была доказана перебором 1936 вариантов. В 2005 её только повторили.
Теорема о корректности системы типов в dependent dependency calculus и прочие удручающе напоминают те самые особенные интегралы, которые можно взять... но которые встречаются только в курсе интегрального анализа.
Очень многие математики относятся к Coq крайне скептически - фактически, он требует просто записывать готовое доказательство, разворачивая все "после тривиальных преобразований получим".
Важное уточнение - учебное пособие приблизительно 40 летней давности. С тех пор индустрия шагнула немного вперёд. И сам курс давно читают с примерами на Python 3.
Эта книга - 1985 года. Тогда ещё даже Mathematica не было.
По сути же - системы доказательств и преобразований из формулы в формулу не особенно популярны за пределами узкого круга тех, кто разрабатывает Coq. Ещё Пуанкаре говорил, что великие математики открывают теоремы - а посредственные математики нужны, чтобы их доказывать.
Если вычислительная математика - то компьютер просто используется как очень мощный калькулятор, там LISP-ов нет, а используется C-подобная CUDA или даже Fortran (на суперкомпьютерах до сих пор). А логическая математика - это крайне узкая область и описание её объектов очень утомительно: приходится разворачивать каждое "после тривиальных преобразований получим". Гротендик и вовсе считал такие инструменты концом математики как науки.
А поддержка JavaScript в этом браузере будет?
Я вот специально зашёл на https://try.scheme.org/ и вбил в строку выполнения
(команда http "GET" get istr ostr)Получил ответ:
ERROR IN console@1:2 -- Unbound variable: |\xd0;\xba;\xd0;\xbe;\xd0;\xbc;\xd0;\xb0;\xd0;\xbd;\xd0;\xb4;\xd0;\xb0;|
Какой-то плохой браузер получился. Мне не подходит.
У меня всё это вызвало стойкое ощущение, что перед нами - эпические усилия по изобретению колеса.
Вот что делает код:
команда пуэп 64 ошибка o8 o16 o8 o8 o16 o16 o16 o8 ostr)???
Он создаёт ошибку? Вызывает ошибку? Почему нельзя записать его как
{
"to": "пуэп",
"cmd": "error",
"list": [
o8, o16, o8, o8, o16, o16, o16, o8],"
ostr": true}
и интерпретировать????
Его можно "передать в систему и не беспокоиться о внутренней реализации?" Кажется, кто-то только что изобрёл Observer, Command и Strategy. А может даже и event-based system и хэш-таблицы.
Макросы? Кто-то изобрёл Interpreter и DSL.
Функции как переменные? Указатели на функции были ещё в C.
Лямбды и создание функций на лету, map и т.п.? Давно есть даже в C++.
Рекурсия никуда не пропадала.
Требования писать функции чисто и по возможности использовать иммутабельность - были ещё в учебниках 1980-х.
Из материалов этой книги довольно ясно следует, что однозначное определение доказательства вообще невозможно. Можно говорить только о тавтологических утверждениях, но пользы от них немного (они не увеличивают знание). Ну или о консенсусе математиков по какому-то вопросу.
Ну и вспоминайте получше кандидатский курс - то неужели там не рассказывают, что до конца неясно, на каких аксиомах основана математическая модель ОТО (понятно, что пространство неэвклидово, но как его описать неясно) и что мы не знаем, выполняется ли там, к примеру, аксиома Архимеда? Однако эта нехватка формализации не мешает вести исследования. Есть даже подходы, которые прямо отрицают важность этих оснований.
То есть великая теорема Ферма до 1995 года не была теоремой? Это новое слово в истории математики.
Из этой заявления следует много не менее странных: например, неясно, как быть с невыводимыми теоремами, которые описываются теоремой Гёделя о неполноте. Их истинность доказать можно, а вывести из аксиом - нельзя.
Вы написали много про меня, и ничего по теме
Если бы вы разбирались в теме, то аргументация звучала бы так:
Scheme и чисто функциональные языки активно применяются в области X. Да, они не подходят для программирования контроллеров, но пример современного использования можно найти в книге Y.
Для примера: вот код, который описывает математическую матрицу средствами Haskell. После того, как вы определили матрицу таким образом, вы можете легко производить над ней операции вот так:
Я допускаю, что вам интересно рассказывать про лемму Йонеды. Но вот что важно: вас про лемму Йонеды и капитализацию криптовалют никто не спрашивал.
Так что я не берусь вам ничего объяснять - потому что мне очевидно, что вы ничего из моих объяснений не поймёте. Вы - гений, вы знаете лемму Йонеды. Нам всем остаётся только внимать такому великому гению, как вы.
Тем, что gcc используется несколько шире.
Заявления каких-то компаний и базворды в их отчётах - так себе аргумент. И тем более их капитализация.
По вашему нет компаний с большей капитализацией, которые используют Visual Basic?
Ну то есть вы предполагаете, что она там есть.
А я предполагаю, что там С++. Или Go. Или Rust. Или Visual Basic. Попробуйте опровергнуть.
Это говорит о том, что никакой "защиты от ошибок" в Хаскелле нет. Раз один городской сумасшедший смог её обойти самым примитивным способом.
Если вы не знаете, как аргументированно опровергать - попробуйте изучить учебник логики для первого курса.
А то как-то обидно получается - рассуждаете о доказательной теории и алгебре, а аргументировать только помойными червями умеете.
Обратитесь к обезьянкам в зоопарке и к помойным червям. Вы явно эксперт в этой области, они с удовольствием вас послушают. Уверен, вы просто раздавите их вашим космическим интеллектом.
То есть в компиляторе всё того же Haskell.
А почему не Hamster Combat? У него тоже была большая капитализация.
Где я могу увидеть этот анализатор? На каком языке он написан?
Я помню, как фейсбуковский антиспам не мог ничего сделать против одного отморозка, который призывал к убийствам и в каждый комментарий вставлял картинку.
Антиспам гордо рапортовал, что на картинке не обнаружено ничего плохого...
Мощная система. И что, тоже на Scheme написана?
Ну то есть вы не знаете, как считается определитель.
Этому обучают на профильных факультетах. Примерно на первом курсе.
Если не шарите - попробуйте восполнить оскорблениями. Расскажите им про помойных червей и обезьянок в зоопарке. Они будут вас внимательно слушать.
Вам стоило бы немного поизучать логику. Аргументация оскорблениями (то у вас обезьянки в зоопарке, то копошение червей у мусорного пакета) - признак небольшого ума.
Думаю, за меня неплохо ответит книжка Имре Лакатоса "Доказательства и опровержения". Там довольно подробно расписана проблема того, как одна тривиальность проваливается в другую.
Поэтому открытие теорем кажется мне более важным, чем их формальное доказательство.
Тем не менее Perl 5 продолжает обновляться и у него на порядок больше пользователей.
Очевидно, он позволяет решить больше задач и более удобен.
К сожалению, мне нет дела до того, какие слова или выражения вы выучили. Будь то "монада", "эндофунктор", "аорист" или "закозельская кукарямба".
Если бы это было важно - это бы нашло применение где-то за пределами случайных проектов в случайных компаниях и академических исследований о заведении лямбды за сигму.
Пока же это просто до зубной боли нудная реклама, обстрел читателя кучей терминов из крайне узких разделов математики и на каждом шагу при попытке узнать подробности наталкиваешься на то, что привычные термины просто переопределены по своему.
Это применяется для написания компиляторов? Каких компиляторов? Как выясняется, это компиляторы из одного диалекта LISP в другой диалект LISP, описанные в мощнейшем университетском курсе 40-летней давности.
Это позволяет писать программы без ошибок? Как выясняется, под программой понимается не приложение, а кусок кода, который ничего не делает или считает ряд Фибонночи.
Это позволяет писать код яснее и короче? Приведённые примеры - что-то инопланетное, из них вообще невозможно понять, что происходит, как это отлаживать и как поддерживать. Как подсчитать определитель у определённой таким образом матрицы - непонятно. Из лемма Йонеды это никак не следует.
Предлагаю вспомнить ещё один успешный проект на Racket - Perl 6.
Им тоже никто не пользуется.
Однако на ООП реализовано множество приложений, которыми мы пользуемся каждый день. В том числе и языковых моделей.
В то время как другие были заняты изучением обезьянок в зоопарке. Возможно, как раз для этой важнейшей задачи Scheme и является крайне востребованным языком.
Удручающе напоминает "великую теория Смысл-Текст" Мельчука и Жолковского. В ABBYY на её основе лет 10 делали систему автоматического перевода - и так и не сделали.
А что такое закозельская кукарямба?
Теорема Пифагора была доказана ещё древними вавилонянами.
Теорема о четырёх красках была доказана перебором 1936 вариантов. В 2005 её только повторили.
Теорема о корректности системы типов в dependent dependency calculus и прочие удручающе напоминают те самые особенные интегралы, которые можно взять... но которые встречаются только в курсе интегрального анализа.
Очень многие математики относятся к Coq крайне скептически - фактически, он требует просто записывать готовое доказательство, разворачивая все "после тривиальных преобразований получим".
Ну я бы сказал, что всё намного проще - с появлением более лаконичных и читаемых языков Scheme отправился вслед за Smalltalk и Simula67
Важное уточнение - учебное пособие приблизительно 40 летней давности. С тех пор индустрия шагнула немного вперёд. И сам курс давно читают с примерами на Python 3.
Эта книга - 1985 года. Тогда ещё даже Mathematica не было.
По сути же - системы доказательств и преобразований из формулы в формулу не особенно популярны за пределами узкого круга тех, кто разрабатывает Coq. Ещё Пуанкаре говорил, что великие математики открывают теоремы - а посредственные математики нужны, чтобы их доказывать.
Если вычислительная математика - то компьютер просто используется как очень мощный калькулятор, там LISP-ов нет, а используется C-подобная CUDA или даже Fortran (на суперкомпьютерах до сих пор). А логическая математика - это крайне узкая область и описание её объектов очень утомительно: приходится разворачивать каждое "после тривиальных преобразований получим". Гротендик и вовсе считал такие инструменты концом математики как науки.