Войти в систему

Home
    - Создать дневник
    - Написать в дневник
       - Подробный режим

LJ.Rossia.org
    - Новости сайта
    - Общие настройки
    - Sitemap
    - Оплата
    - ljr-fif

Редактировать...
    - Настройки
    - Список друзей
    - Дневник
    - Картинки
    - Пароль
    - Вид дневника

Сообщества

Настроить S2

Помощь
    - Забыли пароль?
    - FAQ
    - Тех. поддержка



Пишет Misha Verbitsky ([info]tiphareth)
@ 2023-07-02 07:26:00
Previous Entry  Add to memories!  Tell a Friend!  Next Entry
Настроение: sick
Музыка:Van Der Graaf Generator - Live at Hemel Hempstead 18 12 1975
Entry tags:anti-russia, math

ВСЕГДА ВЫБИРАЙТЕ САМЫЙ УНЫЛЫЙ ВАРИАНТ
Закончил читать курс по гиперкэлеровой геометрии
http://verbit.ru/IMPA/HK-2023/
получилось залихватски, хотя по уму нужен еще семестр,
если б был еще семестр, я б все вообще рассказал.

На реддите репостят текст, из 2021-го года,
где в паре абзацев суммируется
-- "что будет с Россией?"
-- "будет ничего"

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

Запомните этот раз и навсегда, наколите на обратной
стороне век, твердите это всем и каждому, вызубрите
наизусть, это теперь ваша долбанная скрижаль, я ваш
долбанный пророк:

ВСЕГДА ВЫБИРАЙТЕ САМЫЙ УНЫЛЫЙ ВАРИАНТ.

Все так. Страна говно, а говно не тонет
и горит херово.

Привет


(Читать комментарии) - (Добавить комментарий)


[info]zhitel_vershin
2023-07-02 19:22 (ссылка)
Тогда объясните, почему гиперкэлеры -- шляпа.

(Ответить) (Уровень выше) (Ветвь дискуссии)


[info]wieiner_
2023-07-03 10:05 (ссылка)
там намешано несколько(3) "математичеких систем" и нет никаких систем верификации, что измышления над этим конструктивом верные. Этим пользуются математики, чтобы строить свои сложные и вероятно ошибочные измышления.

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

но само по себе постороение красивое. типа обьединения всех видов взаимодействий в физике. по аналогии они (эти всякие "коллаби - яуи -миллсы -янги") сварганили

это если по простому обьяснить.

(Ответить) (Уровень выше) (Ветвь дискуссии)


(Анонимно)
2023-07-03 12:39 (ссылка)
А разгадка одна

нет никаких систем верификации,
нет никаких систем верификации,
нет никаких систем верификации,

И что Миша вот этой Хуйней 30 лет занимается? Он что Ебнутый?

(Ответить) (Уровень выше) (Ветвь дискуссии)


[info]wieiner_
2023-07-03 19:05 (ссылка)
плотят -- занимается, не плотят -- не занимается
(утром деньги - вечером стулья)

(Ответить) (Уровень выше) (Ветвь дискуссии)


(Анонимно)
2023-07-03 19:29 (ссылка)
Я думал он романтик
А он банальный жлоб

(Ответить) (Уровень выше) (Ветвь дискуссии)


[info]wieiner_
2023-07-03 19:46 (ссылка)
не ну романтик,
но за хостинг платить же надо таки

(Ответить) (Уровень выше)


[info]grusha
2023-07-04 00:51 (ссылка)
>у компьютенрных программ хотя бы есть компилятор, чтобы проверить годность "измышления".

Компилятор, разумеется, совсем не для этого, и верифицировать он ничего не может (хотя бы потому, что баги в этих самых компиляторах находят регулярно).

(Ответить) (Уровень выше) (Ветвь дискуссии)


[info]wieiner_
2023-07-04 07:33 (ссылка)
ну ты как всегда, в своем репертуаре: день это ночь, а ночь это день и пробуйте доказать обратное, ЛОЛ.

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

Но Груша висит и не хочет этого кушать!

(Ответить) (Уровень выше) (Ветвь дискуссии)


[info]grusha
2023-07-04 11:09 (ссылка)
Компилятор создан для того, чтобы программа работала, причем по возможности охуенно быстро. О корректности ее работы ни слова.

Верификация типов это верификация типов, а не верификация программы. Компилятор понятия не имеет, что делает программа и зачем. Он может лишь определить, не пытается ли программа выполнять недопустимые операции над переменными таких-то типов (что, конечно, очень хорошо, так как позволяет заранее отлавливать множество мелких технических ошибок), но он понятия не имеет, что за данные программа хранит в этих переменных и зачем, и поэтому он в принципе не способен верифицировать, правильно ли она это делает.

(inb4 Самтаймс, я в курсе про "богатые системы типов".)

Верификация программ (точнее, потуги таковой верификации) это https://en.wikipedia.org/wiki/Formal_verification. Компиляторы ни при чем от слова совсем.

У динамически типизируемых языков вообще нет даже верификации типов, по определению, и это типа фича а не баг. Это, конечно, говорит о том что динамически типизируемые языки следует использовать лишь для написания очень простых вещей, где множеству мелких технических ошибок неоткуда взяться. Т.е. для написания простеньких скриптов, которые по возможности должны быть как можно короче, проще и читабельнее, так что типизация и т.п. усложнения кода только мешают. Математические доказательства тоже не нуждаются в какой-либо формальной верификации, по похожим причинам на самом деле: математические доказательства должны быть как можно проще. Если доказательство слишком сложное, это уже само по себе проблема, так как не очень понятно что оно вообще доказывает, муть какая-то. (А то что в нем в таком случае и вероятность наличия ошибок выше, это лишь побочное следствие.) И в таких случаях следует пытаться расширить теорию новыми абстракциями, чтобы сделать доказательство понятным, разобраться что вообще происходит, узнать что-то новое. А не пытаться эту муть "верифицировать" непонятно зачем.

(Ответить) (Уровень выше) (Ветвь дискуссии)


[info]wieiner_
2023-07-04 12:06 (ссылка)
Вы, уважаемый, слышали о таком термине "Прагматика". Вот это вот то о чем вы говорите, чего у компилятора "нет", этим занимается прагматика. в простейшем элементарном случае, это просто возможность совместной линковки территориализванных в разных модулях типов, возможность их ретерриториализации для совместного использования. но дальше больше. чем богаче система типов тем куртуазнее прагматика.

(Ответить) (Уровень выше) (Ветвь дискуссии)


[info]grusha
2023-07-04 13:38 (ссылка)
Вы хотите сказать: "ок, компилятор не обеспечивает верификацию программы, но ее обеспечивает линкер"? Как говорится, одна новость охуительней другой.

Или вы хотели сказать что-то другое?

(Ответить) (Уровень выше) (Ветвь дискуссии)


[info]wieiner_
2023-07-04 13:57 (ссылка)
я хочу сказать, что надо знать теорию компиляции и я ее знаю. и она нас учит,
что есть три этапа анализа, лексический, сепмантический и прагматический.

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

(Ответить) (Уровень выше) (Ветвь дискуссии)


[info]grusha
2023-07-04 14:55 (ссылка)
Все эти этапы анализа (ну кроме "прагматического", которые вы сами придумали, поэтому неизвестно что он делает) осуществляются с целью в конечном счете сгенерировать код, чтобы программа работала, а не проверить, что она работает правильно. За правильность ее работы отвечает программист, а не компилятор.

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

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

Какая разница, в одном модуле эти типы или в разных? Иными словами, при чем тут вообще линковщик (задача которого, грубо говоря, раскидать символы по адресам памяти, только и всего)?

(Ответить) (Уровень выше) (Ветвь дискуссии)


[info]wieiner_
2023-07-04 15:33 (ссылка)
ну вот обьясню это как раз. а про это же HOTT Воеводского.

что найти путь -- это и есть доказательство правильности.
своего рода логистика кода. линковщик ищет и настраивает пути/адреса.
дальше прихерачиваем нейросети, которые про это же самое и получаем ИИ.
а нейросети, нечто иное как NavMesh. Вы знаете что такое NavMesh?
это типа когда на определенной территории гугл-карты переводят в вектор
все возможные пути из всех во все возможные точки, чтобы ИИ потом просто выбирал оптимальный. Тесла безводителя так работает. правда там нейросеть аппаратная на ПЛИСЕ (FPGA). Просто у меня про это целая теория L4 . Я прав, а вы не правы и можете не спорить. бесполезно. так весь мир работает. че вы мне тут заливаете?

(Ответить) (Уровень выше) (Ветвь дискуссии)


[info]grusha
2023-07-04 16:02 (ссылка)
Я когда-то тоже подобной бредятиной развлекался: https://www.linux.org.ru/forum/development/5513477?cid=5514390

(Ответить) (Уровень выше) (Ветвь дискуссии)


[info]wieiner_
2023-07-04 16:38 (ссылка)
ну чат-гпт же создает программы осмысленные, значит есть критерии верификации этой осмысленности. лан не буду выходить из себя. Ваше мнение @Grusha ,уважаемый, тоже имеет право на существование. Просто Верификация Смыслов -- это вопрос нейросетей и "частотных характеристик", а не Типов и Смыслов. Вот это основной вывод, наверное.

Это вопрос не смысла и типа, а статистики(логистики) и потока, -- верификация программ.

(Ответить) (Уровень выше) (Ветвь дискуссии)


[info]grusha
2023-07-04 18:14 (ссылка)
>ну чат-гпт же создает программы осмысленные

Лол.

(Ответить) (Уровень выше) (Ветвь дискуссии)


[info]wieiner_
2023-07-05 07:34 (ссылка)
создает!

(Ответить) (Уровень выше) (Ветвь дискуссии)


(Анонимно)
2023-07-08 09:19 (ссылка)
а мамка твоя - нет

(Ответить) (Уровень выше)


[info]sometimes
2023-07-04 13:12 (ссылка)
Я подозреваю, что тут может быть как-то замешан изоморфизм Карри-Говарда-Ламбека

Собственно, ровно то же самое, что вы пишете, но про программирование, написано в известной книжке:

Кажется, Хоар сказал, что эстетическая прелесть программы это не
архитектурное излишество, а то, что отличает в программировании
успех от неудачи. Если, решая задачи из этой книги, читатель
почувствует прелесть хорошо написанной программы, в которой «ни
убавить, ни прибавить», и сомнения в правильности которой кажутся
нелепыми, то автор будет считать свою цель достигнутой.

(Ответить) (Уровень выше) (Ветвь дискуссии)


[info]grusha
2023-07-04 13:47 (ссылка)
Я даже припоминаю, что это за книжка.

Но таки нет (no pun intended), в программировании критерии несколько отличаются. Там больше подходят слова другого чела: a program should be as simple as possible (to do its job well), but not simpler.

(Ответить) (Уровень выше) (Ветвь дискуссии)


[info]wieiner_
2023-07-04 14:00 (ссылка)
моя программа должна быть SOLID, все остальное -- брехня! KISSы эти ваши

(Ответить) (Уровень выше)


(Анонимно)
2023-07-04 03:48 (ссылка)
И что, эти системы как-то повлияли на чью-то жизнь? Кто-то восхитился "о, как это охуенно" и мише дали филдза? Или кто-то заорал "да это же наебалово, на вилы его", и мишу выгнали из математики ссаными тряпками? Нет, всем похуй. Эти ваши гиперэклеры не несут никаких последствий. Они не сделают нашу жизнь не слишком плохой, не слишком хорошей. Все будет так же мерзко и скучно как и сейчас.

(Ответить) (Уровень выше) (Ветвь дискуссии)


[info]wieiner_
2023-07-04 12:08 (ссылка)
ну типа троллейбус, да. пока все будет как есть

https://www.youtube.com/watch?v=H6d9U8iDH2g

(Ответить) (Уровень выше)


[info]wieiner_
2023-07-03 10:07 (ссылка)
не тникаких гарантий что через 10 -20 лет они же скажут: "не, все, мы наигрались, это унылое говно неправильно". И купят новую "швабру" и новый "веник"

(Ответить) (Уровень выше) (Ветвь дискуссии)


[info]paperdaemon
2023-07-03 11:14 (ссылка)
Так и делают тащемта. Потом просят новой бумаги и карандашик и давай "интегрировать".

(Ответить) (Уровень выше) (Ветвь дискуссии)

в каждой шутке есть доля шутки
[info]wieiner_
2023-07-03 11:42 (ссылка)
гипсовые головы!

(Ответить) (Уровень выше) (Ветвь дискуссии)

Re: в каждой шутке есть доля шутки
(Анонимно)
2023-07-03 11:59 (ссылка)
– erklang die Stimme aus dem Keller

(Ответить) (Уровень выше)


[info]paperdaemon
2023-07-03 11:31 (ссылка)
Когда надо объяснять, то не надо объяснять (с).

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

(Ответить) (Уровень выше) (Ветвь дискуссии)


[info]wieiner_
2023-07-03 11:45 (ссылка)
угу, а попробуй вылезь с женечкиной кувалдой поперек их "Общего Мнения",
со Своей Логикой. сразу забанят.

https://youtu.be/853ugypwP3Y

(Ответить) (Уровень выше)


(Анонимно)
2023-07-03 12:00 (ссылка)
ты только что адептов Хаоса

(Ответить) (Уровень выше)

(Читать комментарии) -