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

Ура! Ура! Ура! Я видел её только в пересказе Куздры.

Спасибо огромное!

Формальность кода вы просто заменяете формальностью вычисления. У вас вычисление формально, а у меня там тоже спектр формальности вычислений.

В каком смысле "мусор" он принимает на входе? GCCшники и иже с ними вообще считают, что если программа где-то там содержит UB, её можно превращать вообще во всё, что угодно, т.е. сдавать в утиль.

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

тянет на философские  основы всего IT

Они хотели с наскоку сделать язык моделирования (и проектирования) сверхвыского уровня, который бы позволял сразу проекты в коды превращать.
Ну и потерпели неоднократный крах.
И не поняли почему именно потерпели фиаско.
Было решено превратить крах в победу. Типа отказываемся от полной формализации, она не нужна.

На самом деле формализация нужна и желательна.

Нужна, но маленькой части описаний.

В идеале любые описания нужно уметь превращать в код, но это уже будет AGI уровня HLAI, поэтому и крах.
Это основная причина краха.

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

upd
+ виновата многопараметрическая природа объекта оптимизации, которой не избежать.

Но пока нет  AGI уровня HLAI, описания должны быть разной степени формальности, как оно и было уже длительное время у человечества, типа стадии проектирования и прочее.
Поэтому и эскизы пригодятся и список требований и предпроектная стадия и т.д. и т.п.

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

Категорщики и до градиентного спуска добрались, и как обычно пообобщали несколько алгоритмов в одну кучу: https://arxiv.org/abs/2103.01931 😁

Иначе не получилось бы категории 😄

А кто-нибудь хочет поучаствовать в квантовом хакатоне от MIT на последних выходных января? В этом году можно будет впервые поиграть на ионном (!!1) квантовом компьютере от IonQ. Из требований к участникам - Python, Git и немного квантмеха, в идеале - квантовые SDK (Qiskit). 3-5 человек в команде. Если квантовые штуки для вас в новинку, бояться не надо: перед хакатоном будет небольшой воркшоп про квантовые вычисления и про среду разработки.

Примерное расписание:
- пятница 28е - вокршоп, 17:00-20:00 EST (восточное побережье США) = 23:00-02:00 CET (Западная Европа) = 01:00-04:00 МСК
- суббота 29е - хакатон, 9:00-18:00 EST = 15:00-00:00 CET = 17:00-02:00 МСК
- воскресенье 30 - хакатон 9:00-12:00 EST = 15:00-18:00 CET = 17:00-20:00 МСК, после этого судейство, награждение и закрытие

Регистрация до 21 января.
https://www.iquise.mit.edu/iQuHACK/2022-01-28

Что теория типов "думает" по поводу значений по умолчанию? Они задаются какими-то правилами вывода/аксиомами или как?

Допустим, если я на Хаскелле напишу такой код:

let v :: Nat
let v2 :: Nat
v2 = v + 2

Как будет/может действовать система типов (или что то другое) ?

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

ну да, там не переменные, а имена для констант(значений).

Но если я объявляю какое то имя, говорю что у него тип такой-то, то можно ли аксиомой задавать значение по умолчанию для такого имени?

ну или как то ещё?

Ещё раз: синтаксический сахар.

То есть только так?

Если да, то мне ещё предстоит понять почему🤔🧐

Автор языка волен сделать автоматическое преобразование из
v :: Nat
в
v :: Nat = 0