Programming Language Design

08 October 2026 18:26

Я вам пытаюсь сказать что по мне лучше вначале научить ходить, а вы мне лучше сразу в машину.
Да и в целом это вопрос подхода. Будет интересно послушать о результатах лет через 5!
Выбор инструмента может легко определить жизнь, для меня это стало программирование лет в 13.

Programming Language Design

08 October 2026 18:15

Вопрос в том что взрослый отвечает за себя сам, делает он потом пробежку или уверен что не испортит материал.
А ребенок он просто учится и за ним надо следить.

Programming Language Design

08 October 2026 18:14

так дрель вот - тоже порождает лень и вообще все инструменты электрические. и автомобиль порождает ожирение - надо пешком ходить ;)

Programming Language Design

08 October 2026 18:07

Если у типа есть элиминаторы, то в заключении правила uniqueness
v = v
не пишут ибо это не запрещает подсунуть в тип какую-то ерунду. А суть этого правила как раз в том чтобы защитить

Programming Language Design

08 October 2026 18:02

Вы про обозначения или про суть?😁

Programming Language Design

08 October 2026 18:00

Пишут v equiv v, так?

Programming Language Design

08 October 2026 17:58

Это понятно. Но v = v соблюдается везде, поэтому uniqueness rule избыточны

Programming Language Design

08 October 2026 17:54

Ну просто получается Г |- v : T => True, что верно всегда

Programming Language Design

08 October 2026 17:52

Я отвечал в контексте вопроса про uniqueness rule

Programming Language Design

08 October 2026 17:51

Правда если у вас такое выполняется, то у вас в системе глобальная лажа

Programming Language Design

08 October 2026 17:49

Может выполняться. Зависит от остальных правил вашей системы

Programming Language Design

08 October 2026 17:45

Если у вас есть правила дробяме, то каждое правило в agda/lean/rocq будет конструктором индуктивного типа.

Можно начать с того чтобы перевести дроби в такой индуктивный тип.

Programming Language Design

18 June 2026 17:51

Точно работает хорошо, например в .net

Programming Language Design

18 June 2026 16:12

Класс)
А в вм можно будет динамически создавать функции, классы (если предусмотрены) и подобные конструкции?)

Мне это в js безумно нравится

Programming Language Design

18 June 2026 16:06

*вы будете (просто привык на ты)

Programming Language Design

08 October 2026 18:17

...а то что? отрубит себе палец MPC сервером? :) для ребенка 8 лет все объяснение которые в этом чате - белый шум. он учится использовать инструмент. а то что доска для этого молотка из бальзы, а гвозди из обедненного урана ему пока не интересно...

Programming Language Design

08 October 2026 18:15

с автомобилем давно соревновались в скорости перемещения из точки А в точку Б? :)

Programming Language Design

08 October 2026 18:12

В том то и дело, давать ребенку проф пилу или то что может его покалечить так себе идея, вопрос каким вы считаете данный инструмент.
Для меня это инструмент который порождает лень и тупость. Это эффективный инструмент в определенных вещах, но он так же и опасен.
Если конечно не утрировать, он забирает время и потенциал. Ребенку не нужно зарабатывать на этом, ему некуда спешить и.т.д. и.т.п.
Он может прокачивать мозги, мышление, стремление разбираться в сложных вопросах и.т.д. То что у нас в будущем зачастую забирают, так как есть дедлайны, лимиты и много чего еще. Время. Нейронка может помочь сделать продукт. 1 из 10000 получит реальную финансовую или еще какую то выгоду. Возможно когда нейронка будет не справляться, ребенок захочет узнать что то из внутреннего. Стабильнее как мне кажется привить самостоятельное обучение на более прагматичной системе и потом хоть нейронки, хоть С++, хоть что. Идея разработки игр не только в том что бы сделать продукт, в случае ребенка это как минимум 2 реальные науки и + дополнительные прикладные сферы, которые могут показать как будущую профессию, так и реальные склонности к той или иной науке.
Время, время самый ценный ресурс, нейронка дает быстрые результаты и все.
У всех свое видение этого и это нормально. Для кого то нейронка не проф пила которая может покалечить, а игрушечный молоточек.

Programming Language Design

08 October 2026 18:03

Я про суть. Не понял что значит "так не пишут"

Programming Language Design

08 October 2026 18:01

То есть я пишу но в общем так вроде не пишут

Programming Language Design

08 October 2026 17:59

Так в uniqueness не пишут
v = v

И я не пишу

Programming Language Design

08 October 2026 17:57

На всякий случай:
В заключении правила uniqueness rule говорится об эквивалентности значений какого-то типа. Не типов.

Programming Language Design

08 October 2026 17:53

Я спрашиваю в контексте uniqueness rule. Вы задаете для каждого типа значений по отдельности что для них соблюдается эквивалентность. Это значит что в каких-то случаях она не соблюдается. В каких?

Programming Language Design

08 October 2026 17:51

Они могут быть не равными самим себе как NaN конечно, но эквивалентность то более сильное свойство...

Programming Language Design

08 October 2026 17:50

Так погодите, а какие значения в принципе могут быть не эквивалентными самим себе???

Programming Language Design

08 October 2026 17:47

Если оно выполняется при наличии uniqueness rule, то с вашим uniqueness rule какая-то лажа

Programming Language Design

18 June 2026 18:26

Где дотнет строит ast из байткода? Речь о декомпиляторах типа ilspy?

Programming Language Design

18 June 2026 16:37

Примеров бы, без них неясно

Programming Language Design

18 June 2026 16:09

Своя вм.

Можно и на ты😏

Programming Language Design

18 June 2026 16:05

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