Не увидел, там я вижу лишь список поддерживаемых платформ, и они все есть в бэкенде llvm. Соответственно мой вопрос: какие есть платформы из линукса, поддерживаемые бэкендом llvm, но которых нет в этом списке.
У меня сложилось мнение, что человек который написал статью явно не является программистом. То что губит большие проекты с технической точки зрения(а программист может отвечать только за это), это нелинейный рост сложности и технический долг. И по поводу библиотечного кода, и феймворков, как-то совсем не внятно обозначена позиция. Если мы не говорим про потомков left-pad, то во многие эти решения вложены годы, а иногда и десятилетия опыта и экспертизы не самых глупых людей(а возможно как раз тех самых талантливых о чем упоминается в начале статьи). Многие из них лежат в опен сорсе, с адекватными лицензиями, не использовать эти компоненты просто глупо. (если только не NIH синдром и очередная "фатальная ошибка")
Но существующие реализации некоторых компиляторов, собирают ядро на поддерживаевом им наборе архитектур. И тут вспоминается анекдот про математика и воздушный шар.
Уровень исходной(rustmustdie) статьи пробивает пол, хотя я и не фанат раста. Обычно то, что обозначается в статье, как zero runtime, называется bare metal, потому что именно эмбедерам оно и нужно. И ищется как bare metal rust.
PS: о кто-то обиделся и решил в карму плюнуть ) возможно было недопонимание, поправил, речь шла не о статье на хабре
Тогда еще хуже, отличный для этого случая глобальный алгоритм - Дейкстры, или его реализация на регулярной сетки - волновой, гуглится вместе с реализацией за 15 минут. ) Надо только придумать функцию преобразования высоты в стоимость.
Да жадная локальность, которая может завести в тупик, самая большая проблема. Надо либо строить карту, либо использовать глобальный алгоритм(Дейкстры, или его реализация на регулярной сетки - волновой). Если реализовать как волновой, то это будет single source shortest path tree, то достаточно пройти вдоль значений в правой границе и выбрать минимальное, это и будет оптимальный путь из точки до правой границы.
По вашей ссылке, все как раз наоборот, чем больше потоков, тем лучше для АМД - 7zip, шахматы, кодеки. Для остального софта надо смотреть количество загруженных потоков.
Это все сложно, я бы начал с того чтобы зафиттил при помоши МНК наилучшую локальную плоскость, а геодезику на ней до правого края найти тривиально. Если не хватает информации добрасываем квадратичную форму (аналог гессиана)
Да тут вообще не понятно, какие цели у автора. Если исходить из того, что ему надо найти путь до правой границы, и это должен быть локальный алгоритм (подыграем по максимому и предположим так надо). Ну посчитай ты локальный гессиан, найди локальный кратчайший путь до правой границы(наверное можно даже аналитически), будет хотя бы красиво, а не вот это уперся в стенку - повернул. Да и совсем тривиальный алгоритм должен взлететь, считаем градиент, проекция вектора направления на него является оптимальной линейной аппроксимацией локального поведения функции, считаем проекцию для точек кандидатов, выбираем минимум.
PS: совсем хорошая идея, локально находить при помощи МНК наилучшую плоскость, и выбирать на ней минимальный путь до правого края. На таком даже можно наверное диплом сделать, если расписать все это в виде научно-математической лабуды. )
Ссылку не дам, это из моего опыта и общих представлений как это все работает. Но опровергнуть это достаточно легко, надо лишь привести в пример хотя бы одну полностью формально верифицированную систему большого масштаба.
Ну, трудно, ну, долго. Надо — сжал зубы и сделал :) Я просто неоднократно на отладке оказывался на пару суток в позе из хентая между труб где-нибудь в цеху или котельной, отлавливая плавающую неполадку, больше не хочется, лучше я надежности добавлю в мягком кресле и с котом на коленях :)
Если мы рассматриваем это с фундаментальной точки зрения, то самая большая проблема это нелинейный рост сложности верификации при усложнении системы. (даже если мы откинем всякие аргументы про хрупкость, деньги и время) Но проблема еще и в том, что деньги и время являются определяющим при распределении ресурсов на разработку. В обычной разработке, чаще всего чем гнаться за формально верифицированным кодом, эффективнее потратить те же деньги на покрытие тестами и зарплаты более квалифицированным программистам.
А так относительно недавно два Boeing 737 MAX, крашнулись, из-за того что было сделано на "отвали", и это не была проблема софта. И никто не понес ответственность.
Можете посоветовать литературу для самых маленьких? Вот именно момент с автоматическим выводом, а точнее как составить минимальную полную систему аксиом, чтобы он работал, мне и не понятен. С математическими науками у меня не очень.
Isabelle/HOL: A Proof Assistant for Higher-Order Logic
если не понятно, что там написано, то надо начать с книг по матлогике (first order-logic и т.д.)
>Я не очень понимаю, о чем мы спорим. Верификация больших >проектов возможна?
Нет, я вам с самого начала писал, что сложность верификации растет абсолютно нелинейно. И на данный момент теоретический максимум это примерно 10К строк на систему.
>Вроде, тут мы оба сошлись. Верификация кратно увеличит >цену и время разработки? Да, согласен, не будем пока цифры >обсуждать.
Моя позиция, что не кратно, а скорее всего на несколько порядков.
>Стоит ли верифицировать модули для ответственных >применений? Насколько я понял, вы тут не возражаете.
Если это возможно, и экономически целесообразно, то да, не возражаю.
>Расхождение в том, что считать ответственным применением? >Я считаю, что «ответственным» становится не только код по >областям, но и по популярности, то есть правильно >верифицировать библиотеки и инструменты, > ставшие отраслевым стандартом, пусть это и замедлит их >развитие.
Ответственным надо считать, то где есть сопоставимый экономический эффект или могут умереть люди. Пытаться верифицировать правильно, но для большинства софта это абсолютно провальный путь, смотрите пункт 1. Это дорого, долго, хрупко(сложно изменять функционал), и не масштабируемо.
>TLAP для меня лучше тем, что я понимаю, как он работает, а >как работает Агда/Идрис/Ког — не понимаю.
TLA+ это прежде всего модел-чекер, вот это все разделение на модули и проверка условий, это все возможно только в случаи, когда он может перебрать все необходимое пространство состояний, которое имеет склонность к комбинаторному взрыву. Комбинаторный взрыв, это фундаментальное ограничение практически любого софтового модел-чекера. Но конечно, у любого применяемого в индустрии модел-чекера, есть какая-то ниша, где он позволяет что-то решить лучше-проще чем другие. TLAP это расширение позволяющее писать машинно проверяемые доказательства для TLA+ моделей. В более современных системах вроде Isabella/HOL и других, возможно ни просто писать самому доказательства, но так же есть и вполне рабочий автоматический вывод. Подход с использованием прувинга, более масштабируем и менее подвержен комбинаторному взрыву по сравнению с модел-чекингом, но так же и значительно сложнее.
Просто вы так легко пишете про верификацию, различных библиотек и кода, что у меня складывается предположение, что это для вас какие-то абстрактные понятия. Поэтому и предложил написать вам самому хотя бы тривиальную сортировку с доказательством на TLAP, просто для себя, мне предъявлять ничего не нужно. После этого вы скорее всего поняли, насколько тяжело и выстрадано - то что я говорю по поводу хрупкости и масштабируемости. (даже если вопрос денег и времени, вас не интересует, хотя в конечном итоге все сводится именно к этому)
>Стоп, или мы верим обеим оценкам, или не верим ни одной. Из >той же статьи выше верифицированный код стоит в 3-4 раза >дороже традиционного, по сравнению стоимости двух похожих >проектов — 150 против 500 за строчку.
Разрабатывали они это ядро seL4 на основе готового кода, а не с нуля, то есть это просто стоимость добавления верификации по большей части. Мне честно нет никакого желания разбираться, что они там насчитали для традиционной разработки и почему. А вот оценкам для верификации я вполне доверяю, потому что они укладываются в мои собственные оценки, того что я видел. Если мы берем обычный софт, то 15$ баксов за строчку это максимум. Вы же ведь предлагаете обычный софт писать по тем же принципам, а не aero-space?
>Вот по TLA+, раздел «More Complex Examples», но вступление >пропускать не советую. Это верификация алгоритма, для >соответствия кода алгоритму используется подход как в seL4 >или диссере, который я выше приводил.
Ага, все таки, есть там прув-чекер TLAPS, не знаю как уж он там интегрируется с модел-чекером. Проблема в том, что это прув-чекер, то есть сам он ничего доказывать не умеет, по сравнению с Isabelle/HOL это прошлый век, хотя и имеет определенную нишу для применения. Честно, я этот TLAPS не изучал, но чем он лучше той же Agda не особо понятно. Если вы сами хотите разобраться, почему формальная верификация это очень долго и дорого, попробуйте написать доказательство корректности любой сортировки на TLAPS, можете даже подглядеть как это сделано по ссылке которой вы давали, и все сами поймете.
>Что это за функции, как именно будет определяться, кто их выполняет, и > будет ли считаться достаточной работа на неполный день / > совместительство работы в IT-компании – пока что не понятно.
По той информации, что была это будет поле в 255 символов, где сотрудник должен написать какой он не заменимый, а гендир заверить, подписав всю заполненную форму (csv файл) ЭЦП. Все это в основном нужно для МО. Полный рабочий день, необходимое условие.
Так и процессор с ОС, тоже западный продукт, предлагаю перейти на счеты. По поводу "фатального недостатка" постгреса, нет не убедили.
Да, его вытащили. (информация с телеги ITmobilization и минцифры)
Не увидел, там я вижу лишь список поддерживаемых платформ, и они все есть в бэкенде llvm. Соответственно мой вопрос: какие есть платформы из линукса, поддерживаемые бэкендом llvm, но которых нет в этом списке.
А какие не поддерживаются для которых есть бэкенд?
У меня сложилось мнение, что человек который написал статью явно не является программистом. То что губит большие проекты с технической точки зрения(а программист может отвечать только за это), это нелинейный рост сложности и технический долг. И по поводу библиотечного кода, и феймворков, как-то совсем не внятно обозначена позиция. Если мы не говорим про потомков left-pad, то во многие эти решения вложены годы, а иногда и десятилетия опыта и экспертизы не самых глупых людей(а возможно как раз тех самых талантливых о чем упоминается в начале статьи). Многие из них лежат в опен сорсе, с адекватными лицензиями, не использовать эти компоненты просто глупо. (если только не NIH синдром и очередная "фатальная ошибка")
А какой смысл тогда писать на расте, если все его преимущества с ходу отправляются в ведро? А так конечно можно тролейбус_из_буханки.джепег
Но существующие реализации некоторых компиляторов, собирают ядро на поддерживаевом им наборе архитектур. И тут вспоминается анекдот про математика и воздушный шар.
Уровень исходной(rustmustdie) статьи пробивает пол, хотя я и не фанат раста. Обычно то, что обозначается в статье, как zero runtime, называется bare metal, потому что именно эмбедерам оно и нужно. И ищется как bare metal rust.
PS: о кто-то обиделся и решил в карму плюнуть ) возможно было недопонимание, поправил, речь шла не о статье на хабре
Это все исключительно дело вкуса, от того что вы заметете ассемблер под ковер - он никуда не денется.
Нет, уже давно не называется https://www.kernel.org/doc/html/latest/kbuild/llvm.html
Тогда еще хуже, отличный для этого случая глобальный алгоритм - Дейкстры, или его реализация на регулярной сетки - волновой, гуглится вместе с реализацией за 15 минут. ) Надо только придумать функцию преобразования высоты в стоимость.
Да жадная локальность, которая может завести в тупик, самая большая проблема. Надо либо строить карту, либо использовать глобальный алгоритм(Дейкстры, или его реализация на регулярной сетки - волновой). Если реализовать как волновой, то это будет single source shortest path tree, то достаточно пройти вдоль значений в правой границе и выбрать минимальное, это и будет оптимальный путь из точки до правой границы.
По вашей ссылке, все как раз наоборот, чем больше потоков, тем лучше для АМД - 7zip, шахматы, кодеки. Для остального софта надо смотреть количество загруженных потоков.
Это все сложно, я бы начал с того чтобы зафиттил при помоши МНК наилучшую локальную плоскость, а геодезику на ней до правого края найти тривиально. Если не хватает информации добрасываем квадратичную форму (аналог гессиана)
Да тут вообще не понятно, какие цели у автора. Если исходить из того, что ему надо найти путь до правой границы, и это должен быть локальный алгоритм (подыграем по максимому и предположим так надо). Ну посчитай ты локальный гессиан, найди локальный кратчайший путь до правой границы(наверное можно даже аналитически), будет хотя бы красиво, а не вот это уперся в стенку - повернул. Да и совсем тривиальный алгоритм должен взлететь, считаем градиент, проекция вектора направления на него является оптимальной линейной аппроксимацией локального поведения функции, считаем проекцию для точек кандидатов, выбираем минимум.
PS: совсем хорошая идея, локально находить при помощи МНК наилучшую плоскость, и выбирать на ней минимальный путь до правого края. На таком даже можно наверное диплом сделать, если расписать все это в виде научно-математической лабуды. )
Ссылку не дам, это из моего опыта и общих представлений как это все работает. Но опровергнуть это достаточно легко, надо лишь привести в пример хотя бы одну полностью формально верифицированную систему большого масштаба.
Если мы рассматриваем это с фундаментальной точки зрения, то самая большая проблема это нелинейный рост сложности верификации при усложнении системы. (даже если мы откинем всякие аргументы про хрупкость, деньги и время) Но проблема еще и в том, что деньги и время являются определяющим при распределении ресурсов на разработку. В обычной разработке, чаще всего чем гнаться за формально верифицированным кодом, эффективнее потратить те же деньги на покрытие тестами и зарплаты более квалифицированным программистам.
А так относительно недавно два Boeing 737 MAX, крашнулись, из-за того что было сделано на "отвали", и это не была проблема софта. И никто не понес ответственность.
Isabelle/HOL: A Proof Assistant for Higher-Order Logic
если не понятно, что там написано, то надо начать с книг по матлогике (first order-logic и т.д.)
>Я не очень понимаю, о чем мы спорим. Верификация больших >проектов возможна?
Нет, я вам с самого начала писал, что сложность верификации растет абсолютно нелинейно. И на данный момент теоретический максимум это примерно 10К строк на систему.
>Вроде, тут мы оба сошлись. Верификация кратно увеличит >цену и время разработки? Да, согласен, не будем пока цифры >обсуждать.
Моя позиция, что не кратно, а скорее всего на несколько порядков.
>Стоит ли верифицировать модули для ответственных >применений? Насколько я понял, вы тут не возражаете.
Если это возможно, и экономически целесообразно, то да, не возражаю.
>Расхождение в том, что считать ответственным применением? >Я считаю, что «ответственным» становится не только код по >областям, но и по популярности, то есть правильно >верифицировать библиотеки и инструменты,
> ставшие отраслевым стандартом, пусть это и замедлит их >развитие.
Ответственным надо считать, то где есть сопоставимый экономический эффект или могут умереть люди. Пытаться верифицировать правильно, но для большинства софта это абсолютно провальный путь, смотрите пункт 1. Это дорого, долго, хрупко(сложно изменять функционал), и не масштабируемо.
>TLAP для меня лучше тем, что я понимаю, как он работает, а >как работает Агда/Идрис/Ког — не понимаю.
TLA+ это прежде всего модел-чекер, вот это все разделение на модули и проверка условий, это все возможно только в случаи, когда он может перебрать все необходимое пространство состояний, которое имеет склонность к комбинаторному взрыву. Комбинаторный взрыв, это фундаментальное ограничение практически любого софтового модел-чекера. Но конечно, у любого применяемого в индустрии модел-чекера, есть какая-то ниша, где он позволяет что-то решить лучше-проще чем другие. TLAP это расширение позволяющее писать машинно проверяемые доказательства для TLA+ моделей. В более современных системах вроде Isabella/HOL и других, возможно ни просто писать самому доказательства, но так же есть и вполне рабочий автоматический вывод. Подход с использованием прувинга, более масштабируем и менее подвержен комбинаторному взрыву по сравнению с модел-чекингом, но так же и значительно сложнее.
Просто вы так легко пишете про верификацию, различных библиотек и кода, что у меня складывается предположение, что это для вас какие-то абстрактные понятия. Поэтому и предложил написать вам самому хотя бы тривиальную сортировку с доказательством на TLAP, просто для себя, мне предъявлять ничего не нужно. После этого вы скорее всего поняли, насколько тяжело и выстрадано - то что я говорю по поводу хрупкости и масштабируемости. (даже если вопрос денег и времени, вас не интересует, хотя в конечном итоге все сводится именно к этому)
>Стоп, или мы верим обеим оценкам, или не верим ни одной. Из >той же статьи выше верифицированный код стоит в 3-4 раза >дороже традиционного, по сравнению стоимости двух похожих >проектов — 150 против 500 за строчку.
Разрабатывали они это ядро seL4 на основе готового кода, а не с нуля, то есть это просто стоимость добавления верификации по большей части. Мне честно нет никакого желания разбираться, что они там насчитали для традиционной разработки и почему. А вот оценкам для верификации я вполне доверяю, потому что они укладываются в мои собственные оценки, того что я видел. Если мы берем обычный софт, то 15$ баксов за строчку это максимум. Вы же ведь предлагаете обычный софт писать по тем же принципам, а не aero-space?
>Вот по TLA+, раздел «More Complex Examples», но вступление >пропускать не советую. Это верификация алгоритма, для >соответствия кода алгоритму используется подход как в seL4 >или диссере, который я выше приводил.
Ага, все таки, есть там прув-чекер TLAPS, не знаю как уж он там интегрируется с модел-чекером. Проблема в том, что это прув-чекер, то есть сам он ничего доказывать не умеет, по сравнению с Isabelle/HOL это прошлый век, хотя и имеет определенную нишу для применения. Честно, я этот TLAPS не изучал, но чем он лучше той же Agda не особо понятно. Если вы сами хотите разобраться, почему формальная верификация это очень долго и дорого, попробуйте написать доказательство корректности любой сортировки на TLAPS, можете даже подглядеть как это сделано по ссылке которой вы давали, и все сами поймете.
>Что это за функции, как именно будет определяться, кто их выполняет, и
> будет ли считаться достаточной работа на неполный день /
> совместительство работы в IT-компании – пока что не понятно.
По той информации, что была это будет поле в 255 символов, где сотрудник должен написать какой он не заменимый, а гендир заверить, подписав всю заполненную форму (csv файл) ЭЦП. Все это в основном нужно для МО. Полный рабочий день, необходимое условие.
Так вроде просто, windows vs linux, исходите из этого. Даже если и будут какие-то подводные камни, то они скорее всего решаемые.