это известная мутка

это один из способ заработка кодеров - поиск уязвимостей и их «монетарное сопровождение» )

Нет, страдай теперь.

libressl != libssh

Не пиздите, прекрасно в java бывают segmentation fault'ы. Потому что jvm, которая выполняет java-программу, написана на c++. А еще это всё происходит под управлением операционки, ядро которой написано на C.

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

На текущий момент производительность труда никакая, потому что простейшие вещи требуют лютых приседаний. Попробуй написать корректную реализацию какой-нибудь простой структуры данных, например, АВЛ-дерево. Под корректной я имею в виду реализацию с доказанными компилятором свойствами. Можешь даже для начала забить на упорядоченность ключей в узлах, а только закодировать в тип инвариант сбалансированности - «для каждой его вершины высота её двух поддеревьев различается не более чем на 1», для этого даже зависимые типы не нужны. Как напишешь insert - приходи.

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

В то же время на си достаточно обратиться по неверному адресу.

Если для вас это отличие не существенно, это ваше личное дело. Я не настаиваю.

Вот авл дерево https://github.com/jfdm/idris-containers/blob/master/Data/AVL/Tree.idr . Устраивает? Или именно я должен его написать?

В целом поинт в том что библиотеки пишутся программистами более высокой квалификации в любом языке.

Я ещё лишь начинаю что то писать, но даже по моему небольшому опыту совсем не каждая программа требует таких усилий как авл-дерево. Напрактике скорее ситуация такая: среди хаскелеподобного кода встречаются «моменты» которые нужно доказать, часто они довольно просты и решаются реврайтом.

Так что не так страшен чёрт. Батарейки со временем напишутся.

сделать то можно что угодно. но хацкель.... он не красив

ну это уже на вкус и цвет. мне например наоборот кажется очень стройным и логичным.

А что это за патч? Я что то не вижу, чтобы он хоть что то менял, кроме пробелов.

Ни разу. Если вы считаете вход по паролю ненужным, не включайте его.

А так это явно дыра.

Все рептилойды так говорят. И не моргают.

Да нет, там много изменений в коде, если присмотреться.

Просто говнокодеры засунули в один патч правку форматирования и исправление критической уязвимости. Руки из задницы, сэр.

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

«Даёт, если сказать по эльфийский слово „Друг“»

fxd

Вот авл дерево https://github.com/jfdm/idris-containers/blob/master/Data/AVL/Tree.idr . Устраивает? Или именно я должен его написать?

Да, оно самое. Не устраивает по одной простой причине:

||| *Note* When using this Data Structure, the design is such that the
||| tree does not factor in unbalanced trees and so removal of items
||| is not permited.

Если по-русски - `remove` отсутствует. А чтобы написать `insert`, понадобился David Christiansen.

В целом поинт в том что библиотеки пишутся программистами более высокой квалификации в любом языке.

В первом сообщении посыл был

надо, надо idris внедрять в массы.

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

Я ещё лишь начинаю что то писать, но даже по моему небольшому опыту совсем не каждая программа требует таких усилий как авл-дерево. Напрактике скорее ситуация такая: среди хаскелеподобного кода встречаются «моменты» которые нужно доказать, часто они довольно просты и решаются реврайтом

Ну если писать на идрисе, как на хаскеле, то хаскель выигрывает, для меня, в первую очередь наличием `deriving`, а в тех местах, где что-то нужно доказать, можно и синглтонами воспользоваться, пусть и уродски оно выглядит. Хотя, должен признать, ничего, сложнее векторов, мне нужно не было.

Так что не так страшен чёрт. Батарейки со временем напишутся.

Нисколько в этом не сомневаюсь, через N лет это всё будет в мэйнстриме в каком-нибудь C**, но только когда это произойдёт? Судя по тому, что сейчас плюсовики и джявисты писают кипятком от вывода типов, до внедрения завтипов в массы мы можем и не дожить...

Аргумент «зато говнокодеров сразу видно» хороший, если надо разработать ПО для управления ракетой, но плохой для бизнеса в целом.

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

Например, питон ничего выдающегося собой не представляет как языковая система, да и реализация у него откровенно слабая в смысле производительности. Но именно своим «ни о чем» он и добился популярности.

Я питон никогда не изучал в том смысле, как я изучал, например, ассемблер и C++ в ВУЗе, но если надо, я просто открываю сорцы и пишу. С другой стороны, всё, что я изучал в хаскеле, я давно и прочно забыл.

Есть некий постепенный путь проникновения идей в массовое сознание по мере усложнения задач и возникновения потребности в более эффективных инструментах у этого массового сознания. Например, монада — это такая же математическая абстракция, как, скажем, умножение. Умножение людям нужно, однако сейчас всё еще можно прекрасно писать код, не зная, что такое монада.

Сейчас между «кодером обычным» и кодером на хаскеле существует вот такой разрыв на кривой обучения:

          ---
       ---
      |
      |
      |
      |
   ---
---

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

Пока что этот разрыв всё еще достаточно велик. Всё еще можно тасовать инты и получать результат.

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

С некоторыми абстракциями (монады, например), проблема ещё и в том, что требуется развивать особый вид интуиции, чтобы заметить что их можно применить. Из моих мозгов эта интуиция очень быстро выветривается, и требуются значительные усилия, чтобы её восстановить, и я не один такой наверно.

Да, есть такое.

это кусок патча по ссылке выше

не везде это возможно.

Хотя я везде первым делом отрубаю пароли и гссапи, но в принципе, пароль + fail2ban это приемлемое решение.

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

Непорядок, сарказм без тега [sarcazm]?

Я купился, думал, вдруг уже деменция пришла...

gssapi то по что))) для локалки с керберосом самое то.

ну и смысл либы в реализации протокола. но вырубить по умолчанию конечно могли бы...

Если по-русски - `remove` отсутствует. А чтобы написать `insert`, понадобился David Christiansen.
В первом сообщении посыл был..

Попробую объяснить ещё раз.
Вот например стейт машины. О которых речь в топике. Мне кажется что средний хаскелист с опытом вполне осилит разобрать и написать вот это http://docs.idris-lang.org/en/latest/st/examples.html без всяких проблем.

Я нуб и вроде осиливаю. Доказательства же сложных свойств структур данных это большая отдельная тема, которой, посвящён отдельный том в software foundations. Кмк ты это знаешь не хуже меня.

Для данного конкретного случая (не позволить пройти мимо определённого этапа) не нужно читать софтваре фаундейшнс и не нужен экспириенс с доказательствами на коке в 5 лет. Нужно банально прочесть туториал и написать довольно банальную программу.

Ну если писать на идрисе, как на хаскеле, то хаскель выигрывает, для меня, в первую очередь наличием `deriving`, а в тех местах, где что-то нужно доказать, можно и синглтонами воспользоваться, пусть и уродски оно выглядит. Хотя, должен признать, ничего, сложнее векторов, мне нужно не было.

Мне кажется что вот этот пример (хангман) хорошо иллюстрирует как использовать это на практике (правда там эффекты). Ещё есть вот это (сетевое программирование, уже была ссылка), выглядит довольно просто но я не разбирал пока, поэтому не поручусь.

Ещё мне показалось что ты говоришь о некой абстрактной прям вот полной и тотальной верификации всего и вся. Бреди где-то прямо говорит что на практике это некий компромис. И в примере выше пмсм хорошо видно что не так далеко это от хаскеля как кажется.

Ну и да, может и не доживём, это всё довольно абстрактные рассуждения. Но я для себя решил попробовать.

ЗЫ. Да, кстати дерайвинг вроде уже «почти» есть, но надо там как то elab дергать. Туториала вроде нет. Благодаря упомянутому Кристиансену, как я понимаю. Но я так понимаю окончательная реализация похоже ждёт своего героя.

Тебе не приходило на ум поинтересоваться почему в яве никогда не бывает Segmentation Failed?

В яве бывают IndexOutofbounds и NullPointerException. Те же сегфолты, только с лучшей гранулярностью (не на уровне страниц памяти, а на уровне массивов).

Если ты пытался показать, что из-за какой-то лучшей системы типов в яве меньше, чем в C/C++, ошибок в рантайме и они ловятся в компайл-тайме, то ты облажался. Такие же рантайм-проверки.

Сильно подозреваю, что даже на Си можно было бы сделать так, чтобы возникала ошибка типов. Но Си-прогеры слишком заскорузлы и уверены в себе.

Сильно уверены в себе мамкины борщехлёбы, вроде тебя.

В твоём борщехлёбском манямирке видимо нет битовых полей с флагами, которые число твоих типов раздуют сразу в 2ⁿ раз.

а вообще нужны finite state machine с четко задефайненым графом состояний. но только язык который такое сделает - его самого пока не сделали.

ну как же не сделали, сделали, вот, ознакомьтесь пожалуйста

А это ничего, что текущий топик собственно и представляет собой ошибку в переходах в state machine? Нет же, как обычно тут на ЛОР — всё свели к «сишечке — дерьмо»...

gssapi то по что))) для локалки с керберосом самое то.

За то, что я его не использую для доступа по ssh. ;)

Не использую - отключаю ибо имел неприятный опыт нескольких взломов тех серверов, что поднимал кому-то и _всегда_ это были взломы через механизмы, которые не использовались, но остались включеными по дефолту...

почему в яве никогда не бывает Segmentation Failed?

Они там называются VM Heap failure и происходят в основном из-за багов компилятора на вполне себе валидный с точки зрения языка код.

Но да, выстрелить себе в ногу при операциях с памятью в Java гораздо сложнее, тут согласен.

У вас в наборе слов импортозамещение отклеилось :-)

сертифицированные линукс

Там точно также.

А вот ssh на ГОСТ-ах.

IoT? Ах, идоооот! (с)

мамкины борщехлёбы

В твоём борщехлёбском манямирке видимо

Борщ у тебя в голове вместо мозгов.

Аргумент «зато говнокодеров сразу видно» хороший, если надо разработать ПО для управления ракетой, но плохой для бизнеса в целом.

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

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

У меня вообще давно зреет мысль/проект: тесты для определения уровня хаскель программиста. Типа 0-уровень - что то вроде АДТ, list comprehensions, case для maybe, уметь написать функтор, мейби/either как монада. 0+ уроверь - state, maybe, either - function, applicative, monad. 1 уровень (можно брать на работу джуном), монады/функторы/аппликтивы/foldable/traversable для state, maybe, reader, writer. 1+ уровень - знакомоство с некоторыми библиотеками, знакомство с понятием катаморфизма... дальше не знаю, я где то тут..

Т.е. примерно как вот тут https://www.scala-lang.org/old/node/8610 , но составить так же набор формальных тестов, чтобы каждый мог оценить собственный уровень. И каждый наниматель мог легко его поправить (до уникальных примеров), чтобы тестировать пришедшего на работу.

Вот и будет взаимозаменяемость. В ООП пойди пойми как ты там эту архитектуру классов спроектировал, хорошо или плохо. Нужен полноценный ревью. А тут можно автоматизировать, кажется. И получать некоторое представление «на тройку». Ну а потом плюс собеседование.

Т.е. человек в процессе работы (или обучения в ВУЗе) осознаёт необходимость нового интеллектуального инструмента, а инструмент - вот он - уже есть.

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

Если ты пытался показать, что из-за какой-то лучшей системы типов в яве меньше, чем в C/C++, ошибок в рантайме и они ловятся в компайл-тайме, то ты облажался. Такие же рантайм-проверки.

Я хотел показать, что язык имеет свойство, как верно заметил Pinkbyte «при работе с памятью трудно выстрелить себе в ногу».

Арифметика указателей в яве не используется, поэтому там нельзя сделать ошибку такого рода и вызвать Seg. Failed. То что там всё таки используется выделение памяти ручное - да, ведёт к ошибкам связанным с этим. Но вот в хаскеле, например, выделение памяти не используется. Соотвественно NPE не возникает. И это тоже свойство именно языка.

зато можно написать

hi <- withCString "hi" pure

let yo = unsafePerformIO newEmptyMVar
putMVar yo 1
putStrLn =<< takeMVar yo

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

ну, ещё можно просто дёрнуть сишную либу в которой обращение к невалидному указателю. мне таки кажется речь немного не «об том».

попрошу заметить, что первый код, даже не содержит ни одной unsafe операции.

Для поддержки ГОСТа и правда надо пилить отдельный ssh с закладками? Через GSS-API никак?

Кисо обиделось.

Иди к мамочке, она тебя успокоит. Может даже борща нальёт.

Спасибо за замечание. Много думал. Правда ничего не надумал в итоге. Кроме того что надо с особым вниманием относиться к любым си-связанным конструкциям.

всё таки, кажется, штука в том что сам тип CString это не «хаскель-тип» в том смысле что привычные операции с ним (к примеру show) нельзя написать без привлечения ансейф/форин операций. нельзя написать оператор + без привлечения анфейф/форин.

Т.е. я понимаю что система типов в этом примере даёт сбой и хотелось бы как то помечать такие «плохие» типы чтобы их нельзя было передать в обычные операции (но как тогда быть с id например?). Но всё таки пока типы «родные» кажется, такого сделать нельзя. И это, кажется, хорошее свойство.

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

спасибо за замечание

спасибо за спасибо

Да всем глубоко похрен где ВЫ ловили или не ловили сегфолты, мы про java говорим, а не про sleeply4cat. Человек который никогда не запускает jvm вообще не ловит в ней сегфолты, и что? Сходите в багтрекер оракла, их там множество.

Не, вы конечно можете заявить что реализация jvm может быть и не на C++. Окей, тогда дайте ссылку где взять jvm или устройство, способное выполнять java-байткод с доказанным отсутствием сегфолтов.

Джентльмены верят на слово )))