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

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

grusha
2023-07-04 00:51 (ссылка)

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

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

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

wieiner_
2023-07-04 07:33 (ссылка)

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

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

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

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

grusha
2023-07-04 11:09 (ссылка)

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

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

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

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

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

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

wieiner_
2023-07-04 12:06 (ссылка)

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

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

grusha
2023-07-04 13:38 (ссылка)

Вы хотите сказать: "ок, компилятор не обеспечивает верификацию программы, но ее обеспечивает линкер"? Как говорится, одна новость охуительней другой.

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

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

wieiner_
2023-07-04 13:57 (ссылка)

я хочу сказать, что надо знать теорию компиляции и я ее знаю. и она нас учит,
что есть три этапа анализа, лексический, сепмантический и прагматический.

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

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

grusha
2023-07-04 14:55 (ссылка)

Все эти этапы анализа (ну кроме "прагматического", которые вы сами придумали, поэтому неизвестно что он делает) осуществляются с целью в конечном счете сгенерировать код, чтобы программа работала, а не проверить, что она работает правильно. За правильность ее работы отвечает программист, а не компилятор.

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

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

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

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

wieiner_
2023-07-04 15:33 (ссылка)

ну вот обьясню это как раз. а про это же HOTT Воеводского.

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

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

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

wieiner_
2023-07-04 16:38 (ссылка)

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

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

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

	grusha 2023-07-04 18:14 (ссылка)
	>ну чат-гпт же создает программы осмысленные Лол. (Ответить) (Уровень выше) (Ветвь дискуссии)

	wieiner_ 2023-07-05 07:34 (ссылка)
	создает! (Ответить) (Уровень выше) (Ветвь дискуссии)

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

sometimes
2023-07-04 13:12 (ссылка)

Я подозреваю, что тут может быть как-то замешан изоморфизм Карри-Говарда-Ламбека

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

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

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

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.

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

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

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