/pr/ – programming
@f663836fd1594609ada2442e7ca96568
fulmar
2023-05-21 05:01:37
Всё, я окончательно понял почему динамическая типизация уделывает статическую. Потому что все объекты, которыми мы оперируем в программировании, могут быть закодированы с помощью чисел. Например, список чисел может быть закодирован одозначным образом одним числом. Допустим у нас есть какая-то функция от одного аргумента f : N -> N, которая берёт на вход натуральное число и возвращает натуральное число. Какой тип имеет аргумент функции f в таком случае? Очевидно, что просто число, да? Но когда мы ей передаём число, это может быть на самом деле закодированный список чисел. Кто решает список это или нет? Сама функция, т.е. её дефиниция. Если она декодирует входящее число как список чисел, то значит это список чисел, если нет, то нет.
Поэтому аргумент, что статическая типизация избавляет нас от каких-то там багов - чушь полная. Она работает в ограниченном случае только потому что мы сами себя ограничиваем не кодировать числом списки чисел и т.д.
Т.к. числом можно закодировать любой объект, то получается, что тип N - это также и тип списка чисел [N], это и тип функций N -> N, и тип кортежей (N, N), и тип вообще чего угодно.
Поэтому и аргумент, что статическая типизация даёт нам полезную документацию о том, что принимает и возвращает функция, тоже не работает. Мы указали, что f : N -> N, но это нам никак не помогает понять, что функция f ожидает на самом делел закодированный список чисел и производит внутри себя декодирование этого списка.
P.S.
Закодировать список чисел c помощью одного числа очень просто. Есть нумерация Гёделя, но есть ещё более простой способ.
Например, нам нужно закодировать два числа 3 и 5. В бинарном виде это 11 и 101. Мы можем их закодировать следующим числом в бинарном виде:
10_1111_10_110011 (тут символ "_" используется как разделитель для читаемости, т.е. это на самом деле число 10111110110011).
Мы продублировали каждый бит наших чисел и использовали 10 в качестве разделителя между ними. Декодирование происходим следующим образом. Мы читаем попарно биты числа, начиная справа. Если пара битов перестаёт совпадать, то значит число закончилось и начался разделитель. Пропускаем разделитель и продолжаем дальше читать пары битов следующего числа пока они совпадают. Когда они перестают совпадать, то значит второе число закончилось. И т.д. можно закодировать какое угодно количество чисел одним числом.
Поэтому аргумент, что статическая типизация избавляет нас от каких-то там багов - чушь полная. Она работает в ограниченном случае только потому что мы сами себя ограничиваем не кодировать числом списки чисел и т.д.
Т.к. числом можно закодировать любой объект, то получается, что тип N - это также и тип списка чисел [N], это и тип функций N -> N, и тип кортежей (N, N), и тип вообще чего угодно.
Поэтому и аргумент, что статическая типизация даёт нам полезную документацию о том, что принимает и возвращает функция, тоже не работает. Мы указали, что f : N -> N, но это нам никак не помогает понять, что функция f ожидает на самом делел закодированный список чисел и производит внутри себя декодирование этого списка.
P.S.
Закодировать список чисел c помощью одного числа очень просто. Есть нумерация Гёделя, но есть ещё более простой способ.
Например, нам нужно закодировать два числа 3 и 5. В бинарном виде это 11 и 101. Мы можем их закодировать следующим числом в бинарном виде:
10_1111_10_110011 (тут символ "_" используется как разделитель для читаемости, т.е. это на самом деле число 10111110110011).
Мы продублировали каждый бит наших чисел и использовали 10 в качестве разделителя между ними. Декодирование происходим следующим образом. Мы читаем попарно биты числа, начиная справа. Если пара битов перестаёт совпадать, то значит число закончилось и начался разделитель. Пропускаем разделитель и продолжаем дальше читать пары битов следующего числа пока они совпадают. Когда они перестают совпадать, то значит второе число закончилось. И т.д. можно закодировать какое угодно количество чисел одним числом.
@d9c74f7ff44c404a91fcf16815e0bc5c
fulmar
2023-05-21 08:08:31
>В твоём примере типизация не перестаёт быть статической, то что ты интерпритируешь число как что-то ещё, не делает его чем-то другим
Не делает. Но и пользы от типизации в таком случае никакой.
Пример - gcd: N -> N:
gcd(x) = if(first(x) = 0, first(x), gcd(second(x), mod(first(x), second(x))))
где first(x) берёт первое число из закодированной пары, а second(x) - второе.
Как ты глядя только в gcd: N -> N поймёшь, что в эту функцию надо передавать закодированную пару?
Да, это по-прежнему число. Но тебе это никак не помогает как пользователю этой функции. Тебе всё равно нужно понимание как она работает чтобы её корректно использовать, а её тип не может отразить информацию, что она принимает закодированную пару.
Не делает. Но и пользы от типизации в таком случае никакой.
Пример - gcd: N -> N:
gcd(x) = if(first(x) = 0, first(x), gcd(second(x), mod(first(x), second(x))))
где first(x) берёт первое число из закодированной пары, а second(x) - второе.
Как ты глядя только в gcd: N -> N поймёшь, что в эту функцию надо передавать закодированную пару?
Да, это по-прежнему число. Но тебе это никак не помогает как пользователю этой функции. Тебе всё равно нужно понимание как она работает чтобы её корректно использовать, а её тип не может отразить информацию, что она принимает закодированную пару.
@447cadfdf18d4b3482fb609fcad0acc1
fulmar
2023-05-21 08:10:28
*gcd(x) = if(second(x) = 0, first(x), gcd(second(x), mod(first(x), second(x))))
@132d1b8ae6c84c3486b0d12e855f9cf5
fulmar
2023-05-21 08:37:27
Или, например, работаешь ты в комманде разработчиков и джун решил в своей функции f : N -> N вместо Nothing возвращать 0, а ко всем остальным результатам прибавлять единицу. И вот уже у тебя функция не f : N -> Maybe N, а f : N -> N.
Да, заебись всё в теории. Но на практиче тебе нужно следить за джуном чтобы он так не писал и руководствовался "правилами".
Да, заебись всё в теории. Но на практиче тебе нужно следить за джуном чтобы он так не писал и руководствовался "правилами".
@04027d8f35b0459f983394a562839ab4
fulmar
2023-05-21 09:15:37
>Статическая типизация не про то как ты интерпритируешь данные, а про то как машина их интерпритирует.
Не я, а функция в которую я передаю эти данные. Функция - это и есть машина.
>Если ты передаёшь в функцию число в виде текста, fu("сорок два"), то это всё равно строка, а ты говоришь что это число.
Если fu интерпретирует эту строку как 42, то для неё это число, да.
>Нет, это строка, зная свойства типа строка, мы точно знаем что с ней можно делать а что нельзя.
Ничего мы не знаем. Ты не знаешь с какими строками функцию fu будет корректно вызвать, а с какими получится хуйня в результате.
>Но ты всё равно молодец, тебе выдали каску и инструкцию, а ты бьёшь себя молотком по яйцам и такой "Ха-ха, не работает, каска соснула", красава, наебал систему.
Если я в любой случае должен следовать каким-то "правилам", которые не отражены в коде, то нахуй мне тогда такая типизация? С практической точки зрения, да, я могу использовать статическую типизацию чтобы отразить часть этих правил в коде и часто не писать хуйни. Но в глобально-теоритическом смысле это ничтожно.
Не я, а функция в которую я передаю эти данные. Функция - это и есть машина.
>Если ты передаёшь в функцию число в виде текста, fu("сорок два"), то это всё равно строка, а ты говоришь что это число.
Если fu интерпретирует эту строку как 42, то для неё это число, да.
>Нет, это строка, зная свойства типа строка, мы точно знаем что с ней можно делать а что нельзя.
Ничего мы не знаем. Ты не знаешь с какими строками функцию fu будет корректно вызвать, а с какими получится хуйня в результате.
>Но ты всё равно молодец, тебе выдали каску и инструкцию, а ты бьёшь себя молотком по яйцам и такой "Ха-ха, не работает, каска соснула", красава, наебал систему.
Если я в любой случае должен следовать каким-то "правилам", которые не отражены в коде, то нахуй мне тогда такая типизация? С практической точки зрения, да, я могу использовать статическую типизацию чтобы отразить часть этих правил в коде и часто не писать хуйни. Но в глобально-теоритическом смысле это ничтожно.
@4b6f6337d82c4e6e9c160943e51a9f78
fulmar
2023-05-21 09:18:44
>А потом джун решил заменить все латинские "o" на кириллические, потом решит нассать в чайник и включить пожарную сигнализацию в серверной. Действительно придётся за ним постояно следить
С вот этого взольнул в голос. Молодца.
С вот этого взольнул в голос. Молодца.
@5eb1e41818624bce846e44583771571e
fulmar
2023-05-21 09:33:11
Получается, что система типов не может гарантировать корректность программ. Всегда найдётся способ себе выстрелить в ногу. И о чём тогда все эти сказки о формальной верификации с помощью типов? Если все функции кроме нескольких штук можно выразить как функции N -> N, то любой бред может быть охуительно сверифицирован типами.
У меня теперь нет уверенности, что то что было сверифицировано каким-нибудь Coq на самом деле не хуйня.
У меня теперь нет уверенности, что то что было сверифицировано каким-нибудь Coq на самом деле не хуйня.
@78e07e6821c74fc1ab42f6c0d4442ada
fulmar
2023-05-22 09:13:01
@ff975@ff975b0193464ba78b83f5d3f6120731
>тип -- множество элементов. Функция сверифицирована, если для каждого элемента типа получается корректный результат.
>то есть, если для какого-то элемента не получается, то значит она не сверифицирована
Да, ты прав. Насчёт формальной верификации я ерунду сказал.
Например, чтобы верифицировать
gcd(x) = if(second(x) = 0, first(x), gcd(second(x), mod(first(x), second(x))))
нужно доказать теорему
forall x y z, x + y > 0 && z = gcd(pair(x, y)) -> (forall d, (exist n k, x = d*n && y = d*k) -> z >= d).
где функция pair(x, y) кодирует пару чисел в одно число.
То, что мы кодируем пару чисел одним числом, никак не влияет на корректность доказываемой теоремы.
>тип -- множество элементов. Функция сверифицирована, если для каждого элемента типа получается корректный результат.
>то есть, если для какого-то элемента не получается, то значит она не сверифицирована
Да, ты прав. Насчёт формальной верификации я ерунду сказал.
Например, чтобы верифицировать
gcd(x) = if(second(x) = 0, first(x), gcd(second(x), mod(first(x), second(x))))
нужно доказать теорему
forall x y z, x + y > 0 && z = gcd(pair(x, y)) -> (forall d, (exist n k, x = d*n && y = d*k) -> z >= d).
где функция pair(x, y) кодирует пару чисел в одно число.
То, что мы кодируем пару чисел одним числом, никак не влияет на корректность доказываемой теоремы.
@fc7b9e3c874447b39363a6e2b2333b6a
fibonator
2023-05-23 14:54:46
Окончательно понял, почему статическая типизация уделывает динамическую. Использование языка с динамической типизацией не избавляет от необходимости думать о типах, только их нужно держать в голове, в отличии от программ на языках со статической. И если код чуть больше чем три с половиной функции, то становится невозможно что-то писать осмысленное. А если код писался давно или кем-то другим, то вместо того, чтобы что-то писать приходится по 10 раз бегать по одним и тем же кускам кода каждый раз, когда оно используется. Количество рантайм ошибок в программах со статической типизацией не больше, чем количество рантайм ошибок в программах на языках программирования с динамической типизацией.
@f5fb4c88d55e4d4eb247b3bfed29b232
pupkin
2023-05-28 15:59:32
Если так рассуждать, то и ограда на мостах не нужна, ведь если захочешь, то сможешь перелезть через неё и спрыгнуть в воду. И предохранители на автоматах не нужны, потому что можно при желании взять и отстрелить себе ногу.
Еще есть проблема с производительностью, IO-bound можно писать на Питоне, а CPU-bound приходится выводить в сишные библиотеки и плясать с бубном, что не написать в производительном фрагменте for.
Вообще, нельзя сказать, что "пила уделывает молоток" или "молоток уделывает пилу", для разных целей разное больше подходит.
Еще есть проблема с производительностью, IO-bound можно писать на Питоне, а CPU-bound приходится выводить в сишные библиотеки и плясать с бубном, что не написать в производительном фрагменте for.
Вообще, нельзя сказать, что "пила уделывает молоток" или "молоток уделывает пилу", для разных целей разное больше подходит.
@3644b9a4d21f4f00b014a7f8703e9e79
fulmar
2023-05-30 14:55:57
@fc7b9@fc7b9e3c874447b39363a6e2b2333b6a
>Количество рантайм ошибок в программах со статической типизацией не больше, чем количество рантайм ошибок в программах на языках программирования с динамической типизацией.
И в одном и в другом случае количество смысловых ошибок бесконечно, а точнее счётно.
>Количество рантайм ошибок в программах со статической типизацией не больше, чем количество рантайм ошибок в программах на языках программирования с динамической типизацией.
И в одном и в другом случае количество смысловых ошибок бесконечно, а точнее счётно.
@5134e6ff651d410085f212882a445639
fulmar
2023-05-30 15:31:49
@f5fb4@f5fb4c88d55e4d4eb247b3bfed29b232
>Если так рассуждать, то и ограда на мостах не нужна, ведь если захочешь, то сможешь перелезть через неё и спрыгнуть в воду. И предохранители на автоматах не нужны, потому что можно при желании взять и отстрелить себе ногу.
Уже говорил выше: "С практической точки зрения, да, я могу использовать статическую типизацию чтобы отразить часть этих правил в коде и часто не писать хуйни. Но в глобально-теоритическом смысле это ничтожно."
>Вообще, нельзя сказать, что "пила уделывает молоток" или "молоток уделывает пилу", для разных целей разное больше подходит.
Да. Но тут можно контрить, что аналогия некорректная. Можно сказать, что "смартфон уделывает калькулятор".
>Если так рассуждать, то и ограда на мостах не нужна, ведь если захочешь, то сможешь перелезть через неё и спрыгнуть в воду. И предохранители на автоматах не нужны, потому что можно при желании взять и отстрелить себе ногу.
Уже говорил выше: "С практической точки зрения, да, я могу использовать статическую типизацию чтобы отразить часть этих правил в коде и часто не писать хуйни. Но в глобально-теоритическом смысле это ничтожно."
>Вообще, нельзя сказать, что "пила уделывает молоток" или "молоток уделывает пилу", для разных целей разное больше подходит.
Да. Но тут можно контрить, что аналогия некорректная. Можно сказать, что "смартфон уделывает калькулятор".
@c2f72ad4e8574570957750db4fcdfd30
fibonator
2023-05-30 20:36:57
>Поэтому и аргумент, что статическая типизация даёт нам полезную документацию о том, что принимает и возвращает функция, тоже не работает.
В питоне придумали целый формат комментариев с описанием типов для целей документации.
В питоне придумали целый формат комментариев с описанием типов для целей документации.
@07abbb2282174819a8c00a979e720bd5
fibonator
2023-05-31 20:34:53
>Да. Но тут можно контрить, что аналогия некорректная. Можно сказать, что "смартфон уделывает калькулятор".
Ха-ха, калькулятор иногда лучше. Вот, например, динамически типизируемый питон вполне вместо какого-нибудь ямла может быть. Но программы на нем писать это пиздец, конечно.
Ха-ха, калькулятор иногда лучше. Вот, например, динамически типизируемый питон вполне вместо какого-нибудь ямла может быть. Но программы на нем писать это пиздец, конечно.
@e7b70063f6d3425285a8034d43831517
pupkin
2023-05-31 22:39:18
@5134e@5134e6ff651d410085f212882a445639
> Но в глобально-теоритическом смысле это ничтожно
Да, но теоретический смысл тут неважен. С его точки зрения все языки эквивалентны машине Тьюринга. Ну и нафиг они нужны, давайте лучше кареткой по ленте елозить и граф переходов состояний программировать.
> Но тут можно контрить, что аналогия некорректная
Можно, поэтому приведу примеры, когда каждый тип языков лучше. Если важны скорость и корректность, то лучше статическая типизация. А если простота написания (хуяк хуяк и продакшн), то динамическая. Исследователям и аналитикам в Jupyter Notebook на питончике самое то экспериментировать.
> Но в глобально-теоритическом смысле это ничтожно
Да, но теоретический смысл тут неважен. С его точки зрения все языки эквивалентны машине Тьюринга. Ну и нафиг они нужны, давайте лучше кареткой по ленте елозить и граф переходов состояний программировать.
> Но тут можно контрить, что аналогия некорректная
Можно, поэтому приведу примеры, когда каждый тип языков лучше. Если важны скорость и корректность, то лучше статическая типизация. А если простота написания (хуяк хуяк и продакшн), то динамическая. Исследователям и аналитикам в Jupyter Notebook на питончике самое то экспериментировать.
@6fbb061faea54f5196cd7374ff703617
pupkin
2023-05-31 22:45:04
@c2f72@c2f72ad4e8574570957750db4fcdfd30
> В питоне придумали целый формат комментариев с описанием типов для целей документации.
Это ты про аннотации?
def gcd(a : Integer, b : Integer)
Они еще могут быть полезны, чтобы IDE по ним понимала, когда ты не тот тип передаешь в функцию, и подсказывала. А в рантайме они не проверяются.
> В питоне придумали целый формат комментариев с описанием типов для целей документации.
Это ты про аннотации?
def gcd(a : Integer, b : Integer)
Они еще могут быть полезны, чтобы IDE по ним понимала, когда ты не тот тип передаешь в функцию, и подсказывала. А в рантайме они не проверяются.
@2913c44ed99d4ce79691c8ec355bb48c
fibonator
2023-06-03 20:31:18
@6fbb0@6fbb061faea54f5196cd7374ff703617
это тоже, но еще docstring тоже
это типы исключительно для целей документации, что говорит о том, что они для этого нужны, вопреки утверждению в начале треда
это тоже, но еще docstring тоже
это типы исключительно для целей документации, что говорит о том, что они для этого нужны, вопреки утверждению в начале треда
@1259684f52ac43e49ff5367afc4e6de6
fulmar
2023-07-04 08:34:23
@c2f72@c2f72ad4e8574570957750db4fcdfd30 Там ещё gradual typing запилили. Мне кажется gradual typing не плохая идея. Сбалансированный подход.
@18c20d72db05456aace5d3b3b78d44c8
fulmar
2023-07-04 08:51:56
@07abb@07abbb2282174819a8c00a979e720bd5
>Ха-ха, калькулятор иногда лучше.
Может быть. Калькулятор всегда готов к использованию, не нужно разблокировать экран, искать иконку с приложением, кликать её. У калькулятора дольше батарея держится, а если на солнечных батареях, то он вообще вечен. Он меньше весит. Он не срёт возможно опасными, а может и нет, излучениями. У него могут быть большие физические кнопки, что хорошо для престарелых людей.
Но на практике мы видим, что 99% себе его не будут покупать потому что его задачи покрываются сматрфоном/компом. В этом смысле уделывает.
>Вот, например, динамически типизируемый питон вполне вместо какого-нибудь ямла может быть.
Тюринг полные кофиги? Страшна. Но почему бы и да.
>Ха-ха, калькулятор иногда лучше.
Может быть. Калькулятор всегда готов к использованию, не нужно разблокировать экран, искать иконку с приложением, кликать её. У калькулятора дольше батарея держится, а если на солнечных батареях, то он вообще вечен. Он меньше весит. Он не срёт возможно опасными, а может и нет, излучениями. У него могут быть большие физические кнопки, что хорошо для престарелых людей.
Но на практике мы видим, что 99% себе его не будут покупать потому что его задачи покрываются сматрфоном/компом. В этом смысле уделывает.
>Вот, например, динамически типизируемый питон вполне вместо какого-нибудь ямла может быть.
Тюринг полные кофиги? Страшна. Но почему бы и да.
@5c9ae09204f64786be246a4eb9bd8886
fulmar
2023-07-04 09:20:59
@e7b70@e7b70063f6d3425285a8034d43831517
>Да, но теоретический смысл тут неважен. С его точки зрения все языки эквивалентны машине Тьюринга.
Я имею в виду, что мы всё равно продолжаем существовать в мире не отражённых в коде правил корректного написания программ. Не важно динамическая это типизация или нет. Поэтому, если даны две эквивалетные проги, одна на статике, другая на динамике, нет никаких гарантий, что одна из них будет корректнее другой. Это больше зависит от адекватности кодеров её писавших. Но даже если предположить, что её написала одна и та же команда людей, не может быть точного ответа о корректности. Если нет формальной верификации, то что одно, что второе - куча говнокода и хер его знает насколько оно корректно.
>Да, но теоретический смысл тут неважен. С его точки зрения все языки эквивалентны машине Тьюринга.
Я имею в виду, что мы всё равно продолжаем существовать в мире не отражённых в коде правил корректного написания программ. Не важно динамическая это типизация или нет. Поэтому, если даны две эквивалетные проги, одна на статике, другая на динамике, нет никаких гарантий, что одна из них будет корректнее другой. Это больше зависит от адекватности кодеров её писавших. Но даже если предположить, что её написала одна и та же команда людей, не может быть точного ответа о корректности. Если нет формальной верификации, то что одно, что второе - куча говнокода и хер его знает насколько оно корректно.
@5102553e0d9b4c14b2e41356ae8119c4
pupkin
2023-07-08 08:15:51
@5c9ae@5c9ae09204f64786be246a4eb9bd8886
У тебя какое-то чёрнобелое видение. Либо формально верифицированный код, либо непонятная куча говнокода. От статической типизации вероятность ошибки не сведется к нулю, но значительно уменьшится. И код будет проще читать и проверять. А с практической точки зрения это и важно.
У тебя какое-то чёрнобелое видение. Либо формально верифицированный код, либо непонятная куча говнокода. От статической типизации вероятность ошибки не сведется к нулю, но значительно уменьшится. И код будет проще читать и проверять. А с практической точки зрения это и важно.
@186cbd4413eb4ae6beaccb3c7d217c46
pupkin
2023-07-08 08:17:22
Ты же не будешь утверждать, что код на Си и код на Брейнфаке это одно и то же? Хотя с теоретической точки зрения это так.
@5b11d8a1de9c4290aa69e7bc54f64549
fulmar
2024-01-29 09:36:17
@5ae3f@5ae3f74a104041f18f7c37a674034218
>Дело вкуса, но на моей практике питон сложнее читать, чем что угодно практически. Именно потому что нет типов. Все выглядит как: все есть хуй знает что, хуй знает что друг с другом сообщается посредством хуй знает чего.
Тоже так раньше думал. Но не только про питон, про все динамически типизируемые языки. Правда где-то посередине видимо.
На типизируемых языках тоже можно написать так, что хрен поймёшь. Какой-нибудь object на вход приходит - хер знает что это может быть, надо смотреть код. Вместо енамки число передаётся - тоже хер поймёшь не зная контекста. Хорошо когда код только ты один пишешь, тогда может быть да - типизация выступает как полезный инструмент дающий дополнительную информацию. Но с другой стороны, что мешает документацию нормальную писать для кода на динамически типизируемом языке.
>Дело вкуса, но на моей практике питон сложнее читать, чем что угодно практически. Именно потому что нет типов. Все выглядит как: все есть хуй знает что, хуй знает что друг с другом сообщается посредством хуй знает чего.
Тоже так раньше думал. Но не только про питон, про все динамически типизируемые языки. Правда где-то посередине видимо.
На типизируемых языках тоже можно написать так, что хрен поймёшь. Какой-нибудь object на вход приходит - хер знает что это может быть, надо смотреть код. Вместо енамки число передаётся - тоже хер поймёшь не зная контекста. Хорошо когда код только ты один пишешь, тогда может быть да - типизация выступает как полезный инструмент дающий дополнительную информацию. Но с другой стороны, что мешает документацию нормальную писать для кода на динамически типизируемом языке.
@46210579a4024c5782e88cd94c9af835
fulmar
2024-01-29 10:58:24
@51025@5102553e0d9b4c14b2e41356ae8119c4
>От статической типизации вероятность ошибки не сведется к нулю, но значительно уменьшится.
Это предположение, которое сложно проверить. Да, так может казатся, что вероятность меньше, но может это только кажется.
>И код будет проще читать и проверять.
Ну вот представь читаешь ты код на статически типизированном языке, а там в функцию передаётся строка и подразумевается, что в ней должен быть json. Типизация тебе не говорит ничего об этом, ни то какая там схема у этого жсон, ни то что там вообще жсон.
>От статической типизации вероятность ошибки не сведется к нулю, но значительно уменьшится.
Это предположение, которое сложно проверить. Да, так может казатся, что вероятность меньше, но может это только кажется.
>И код будет проще читать и проверять.
Ну вот представь читаешь ты код на статически типизированном языке, а там в функцию передаётся строка и подразумевается, что в ней должен быть json. Типизация тебе не говорит ничего об этом, ни то какая там схема у этого жсон, ни то что там вообще жсон.
@a79f972959e4475fa5bfdc8b331d9bb5
fulmar
2024-01-29 11:14:18
@186cb@186cbd4413eb4ae6beaccb3c7d217c46 Вообще это интересный вопрос, но немного не в тему. Смотря про какую одноитожесть речь. Понятно, что на любом тьюринг полном языке можно написать интерпретатор любого другого языка, но ты будешь выполнять тогда код написанный на этом другом языке, а не изначальном.
@b9fc4d1bda9c43dcb4aa40718b057840
julia
2024-05-07 23:46:35
@46210@46210579a4024c5782e88cd94c9af835
> Это предположение, которое сложно проверить.
Да, это сложно проверить статистически. Оно вытекает из рационалистической предпосылки о том, что долгосрочная (> 10 лет) эволюция технологий и человеческого знания работает на увеличение ERoEI. Типа если без статической типизации было норм писать программы, то зачем ее создали и как она до сих пор живет в ЯПах в т.ч. для продакшена? Динамическая и статическая типизации появились не вчера, они есть как в самых старых (Ассемблер - пример динамической типизации) так и в самых новых ЯПах (Rust - пример удавшейся статической типизации).
> Типизация тебе не говорит ничего об этом, ни то какая там схема у этого жсон, ни то что там вообще жсон.
Правильно. Потому что типизация - это инструмент верификации структуры одной программы. В контексте гетерогенных систем она не имеет смысла. Программа X просто не может перед запуском проверить, что ей присылает программа Y, у которой свои соглашения.
@f5fb4@f5fb4c88d55e4d4eb247b3bfed29b232
На мой взгляд, тут более уместна аналогия: "зачем нужна машина, если до необходимого можно любым средством передвижения дойти и на машине гибнут не меньше чем пешеходы?". Если бы только всё так было просто...
@5134e@5134e6ff651d410085f212882a445639
> Но в глобально-теоритическом смысле это ничтожно
"Глобально-теоретический смысл" не имеет инженерной ценности. Типизация - имеет.
> Это предположение, которое сложно проверить.
Да, это сложно проверить статистически. Оно вытекает из рационалистической предпосылки о том, что долгосрочная (> 10 лет) эволюция технологий и человеческого знания работает на увеличение ERoEI. Типа если без статической типизации было норм писать программы, то зачем ее создали и как она до сих пор живет в ЯПах в т.ч. для продакшена? Динамическая и статическая типизации появились не вчера, они есть как в самых старых (Ассемблер - пример динамической типизации) так и в самых новых ЯПах (Rust - пример удавшейся статической типизации).
> Типизация тебе не говорит ничего об этом, ни то какая там схема у этого жсон, ни то что там вообще жсон.
Правильно. Потому что типизация - это инструмент верификации структуры одной программы. В контексте гетерогенных систем она не имеет смысла. Программа X просто не может перед запуском проверить, что ей присылает программа Y, у которой свои соглашения.
@f5fb4@f5fb4c88d55e4d4eb247b3bfed29b232
На мой взгляд, тут более уместна аналогия: "зачем нужна машина, если до необходимого можно любым средством передвижения дойти и на машине гибнут не меньше чем пешеходы?". Если бы только всё так было просто...
@5134e@5134e6ff651d410085f212882a445639
> Но в глобально-теоритическом смысле это ничтожно
"Глобально-теоретический смысл" не имеет инженерной ценности. Типизация - имеет.
@01fb1bff5d3346939f4714e18187069a
fulmar
2024-08-26 17:35:21
@b9fc4@b9fc4d1bda9c43dcb4aa40718b057840
>Типа если без статической типизации было норм писать программы, то зачем ее создали и как она до сих пор живет в ЯПах в т.ч. для продакшена?
Потому что некоторым людям кажется, что она помогает.
>Программа X просто не может перед запуском проверить, что ей присылает программа Y, у которой свои соглашения.
Можно же привести пример и с одной программой. Например, ты хранишь индексы на элементы в массиве (или какие-нибудь ключи хеш таблицы или ещё какие-нибудь айдишники.) Таким оразом ты выключаешь типизацию вообще, потому что сам индекс не говорит тебе что он индексирует, какой там тип элемента и есть ли вообще ещё там именно тот объект по этому индексу (если нет, то это аналог use after free) и т.д. Так можно и borrow checker раста обойти, кстати.
>Типа если без статической типизации было норм писать программы, то зачем ее создали и как она до сих пор живет в ЯПах в т.ч. для продакшена?
Потому что некоторым людям кажется, что она помогает.
>Программа X просто не может перед запуском проверить, что ей присылает программа Y, у которой свои соглашения.
Можно же привести пример и с одной программой. Например, ты хранишь индексы на элементы в массиве (или какие-нибудь ключи хеш таблицы или ещё какие-нибудь айдишники.) Таким оразом ты выключаешь типизацию вообще, потому что сам индекс не говорит тебе что он индексирует, какой там тип элемента и есть ли вообще ещё там именно тот объект по этому индексу (если нет, то это аналог use after free) и т.д. Так можно и borrow checker раста обойти, кстати.
@be5ed623ea5e41b29c7b74a1184264d3
fulmar
2025-06-21 20:18:12
С формальной верификацией кода и продвинутыми системами типов я вижу следующие проблемы. Спецификация может быть не полной и описывать не все возможные свойства. Поэтому тот факт, что программа была формально верифицирована ещё ничего не значит. Важно ещё качество самой спецификации. Спецификация программы может быть (и часто так и есть) почти такой же сложной в описании как и сама программа которую она описывает. А значит возможны ошибки в самой спецификации - она описывает не то, что нужно.
@cf326d86e54944dfb4ebf22a1b9944b6
fulmar
2025-06-21 21:15:04
Пример - функция сортировки, которая формально верифицирована как "возвращающая отсортированный массив", но спецификация не учитывает, что массив должен содержать те же элементы, что и исходный. Результат - программа, которая всегда возвращает пустой массив, технически удовлетворяет спецификации.
Даже для простых функций спецификации могут быть сложнее или сопоставимы по сложности с реализацией:
Даже для простых функций спецификации могут быть сложнее или сопоставимы по сложности с реализацией:
/*@ requires valid_string(src);
@ requires \valid(dest + (0..strlen(src)));
@ requires \separated(dest + (0..strlen(src)), src + (0..strlen(src)));
@ assigns dest[0..strlen(src)];
@ ensures valid_string(dest);
@ ensures strcmp(dest, src) == 0;
@*/
char* strcpy(char* dest, const char* src);
@b02805b465c64348b4204a75d893cb36
fibonator
2025-06-22 23:09:57
@be5ed@be5ed623ea5e41b29c7b74a1184264d3 а если космический луч в ячейку памяти попадет
@d2f738d8845848f9a3dc26cf61e572ac
fibonator
2025-06-22 23:14:07
@be5ed@be5ed623ea5e41b29c7b74a1184264d3 допустим доказанно корректный компилятор компилирует доказанно корректную программу на доказанно корректной ОС делает необозримые вычисления и говорит, что теорема верна. Можно ли ему верить?
@d82052c3a1dd4b20a5c1ec00310459a9
fulmar
2025-06-23 00:35:05
@b0280@b02805b465c64348b4204a75d893cb36 если есть экранирование, ECC, радиационно-стойкая электроника - вероятность этого события будет почти 0 (на земле).
@6fd80d1436fb43d1af2c3faa2678d543
fulmar
2025-06-23 00:37:04
*вероятность ошибки
@e463c4b4df6b49658eb8cb7bd16abd18
fulmar
2025-06-23 09:13:45
@d2f73@d2f738d8845848f9a3dc26cf61e572ac It depends. Спецификация компилятора и программы полные или нет, есть ли в них баги? Пусть пруф покажет.