Нашли или выдавили из себя код, который нельзя назвать нормальным,
на который без улыбки не взглянешь?
Не торопитесь его удалять или рефакторить, — запостите его на
говнокод.ру, посмеёмся вместе!
Только вот нахуя тут только xorb определен через этот паттерн-матчинг, а прочая хуита через какой-то if then else? xorb тоже можно через if-else питушню завернуть. И почему тут стрелки Пирса нет?
Х.з., видимо нотации показались более удобными. Они и при отладочном выводе работают в обратную сторону, в отличие от универсальных гомоикон. Ну и на ядро никак не влияют.
А ltac тьюринг полный, что в ядро тащить вообще нельзя.
В том, что в гомоиконщине под "макросом" обычно понимается нечто большее, с гораздо более широким функционалом по трансформации данных. Можно перехачить аргументы до неузнаваемости или вообще по сети куда-то сходить и воткнуть ответ сервера...
Т.е. если "нотация" -- это "макрос", то очень-очень ограниченный.
Ну так можно использовать подмножество возможностей макросов.
Можно даже сделать специальный макрос, который принимает макрос в качестве аргумента и убеджается в том, что этот макрос соответствует некоторым критериям, и вот только тогда он в что-то раскрывается. А иначе ошибка компиляции.
Не вижу проблемы короче. Вот если б наоборот, макросы были более ограничеными...
если во время применений тактик допустить какие-то дополнительные вычисления в контексте и цели, то не совсем понятно, что именно показывать пользователю. если же это происходит во время вызова Qed и Defined, когда строится сам терм, то это все вообще в черный ящик превращается. нотации хороши, потому что просты и тупы
Т.е. проблема гомоиконушни в том, что она умеет больше, чем "нотации"? Ну так можно ограничить "макросы", чтобы они работали максимум как "нотации". Т.е. ввести специально ограниченные макросы под это.
> Once you understand that Lisp code is data (lists of atoms), you realize that you can use read to read in Lisp code as data. And since Lisp comes with a set of functions for elegantly processing lists, suddenly it's really easy to parse Lisp code.
> You just wrote a parser that turns all define expressions into lambda expressions.
> That should impress you. How would you do that in Python? Or Javascript? You need access to the AST and need to learn all the internal methods for parsing it. Lisp code is an AST.
а в чем тогда поинт вводить макросы, если они будут ограничены? только еще придется писать обратный макрос, чтобы не получить где-то смачный развернутый терм в миллион строк. а не няшную нотацию
> а в чем тогда поинт вводить макросы, если они будут ограничены?
А суть не в макросах, а в однородном синтаксисе. Полноценные макросы могут тоже присутствовать, только они могут раскрываться как какой-нибудь сишный препроцессор, и потом уже над "раскрытым" представлением можно делать какие-то манипуляции.
Зачем однородный синтаксис? Чтобы удобно конструировать и читать это всё, чтобы можно было удобно это в что-то другое экспортнуть. Чтобы не держать в голове правила приоритетов каких-то операций, и что какая-то там функция может быть размазана на несколько "инфиксных операций". Вот например https://coq.inria.fr/refman/language/coq-library.html#init-notations
Тут есть такая штука "_ <= _ <= _" напоминающая какой-то японский смайлик. А по-сути эта функция от трех аргументов, которая про "(a <= b) && (b <= c)" А в каком-нибудь лиспе это можно записать как (and (<= a b) (<= b c)) и это дерево.
_ and
/ \
<= <=
/ \ / \
a b b c
И я допустим могу по этому дереву ходить какими-то "итераторами" и что-то в нем добавлять/переставлять, это просто и понятно. А зачем это делать через два инфиксных оператора? И еще приоритеты какие-то? Зачем? Зачем?
Хотя этот "_ <= _ <= _" конечно можно и в макрос завернуть, например что-то типа "(@N a <= b <= c)" и вот этот "@N" будет пытаться заманчить чем-то это, найдет правило и перепишет на "(and (<= a b) (<= b c))"
Но проблемы с приоритетом операций тут не будет, и такой макрос до раскрытия тоже можно рассматривать как дерево
. _____@N______
/ | | | \
a <= b <= c
А как мне рассматривать "как дерево" эти нотации с приоритетами?
Сам движок у коки, насколько понимаю, как раз работает с однородным and (le a b) (le c d). Он ничего не знает ни про инфиксные операторы и их приоритеты ни про прочие нотации.
Просто для удобства пользователя эта штука вводится и выводится как a <= b <= c.
Не нравятся нотации? Выруби их в переменной или галочкой в IDE. Будешь читать портянки говна именно так, как их видит прувер.
Правда вместо чисел у тебя будут S (S (S (S O)))). Но это ведь мелочи...
> Не нравятся нотации? Выруби их в переменной или галочкой в IDE. Будешь читать портянки говна именно так, как их видит прувер.
А почему б пруверу сами эти нотации не видеть как дерево, и не оттранслировать теоремы-леммы в теоремы-леммы в терминах этой другой нотации? Например, если мне надо что-то доказать, что завязано на десятичную систему счисления, ну скажем https://ru.wikipedia.org/wiki/Проблема_196
и вот я описываю правила отображения S (S (S ... в какой-то там (DEC 1 9 6), и этот S ( S ( S ... может сложиться в этот DEC и наоборот. И описываю теорему про (DEC 1 9 6) и пруваю в терминах этой же нотации
> Правда вместо чисел у тебя будут S (S (S (S O)))). Но это ведь мелочи...
А обязательно ли числа "хранить" такой питушней в представлении для прувера? Можно ж как-нибудь
> Нет, но эта форма очень удобна для индуктивных пруфов.
А если у тебя какое-то очень большое число, которое в S (S (S (S ... форме не будет помещаться в оперативной памяти? Например, если ты захочешь взять самое большое число, для которого доказана его простота, и захочешь это проверить в Coq, как ты с этим числом будешь работать?
> Не нравятся нотации? Выруби их в переменной или галочкой в IDE. Будешь читать портянки говна именно так, как их видит прувер.
Мне в нотациях не нравится, что там какие-то "приоритеты" и "ассоциативность" есть, которые надо иметь в виду для понимания смысла. Можно сделать нотации на макросне, где ничего такого нет. Вот вместо "a <= b <= c" сделать "(@N a <= b <= c)" - и нету никаких проблем с ассоциативностью. Если надо записать "a <= b <= c + d" то просто пишешь "(@N a <= b <= (@N c + d))" и нет никаких неоднозначностей.
И эту макросню точно так же можно зажимать и разжимать
Так или иначе, утверждение "Синтаксис — это самая неинтересная и иррелевантная часть любого ЯП." я считаю хуйней. Синтаксис можно сделать говноуебанским и кривым, со всякими неочевидными говноправилами и требующим какого-то суперизъебского парсера чтобы это говно разобрать, и язык от такого говносинтаксиса будет неюзабельным куском дерьма.
> А как мне рассматривать "как дерево" эти нотации с приоритетами?
Дык всё просто...
Я пишу a <= b <= c. Петух это видит как and (le a b) (le b c), но выводит мне как a <= b <= c.
Я пишу remember (a <= b) as d. Петух видит результат этой замены как and d (le b c), но выводит мне d /\ b <= c.
> Я пишу a <= b <= c. Петух это видит как and (le a b) (le b c), но выводит мне как a <= b <= c.
А если ты напишешь "and (le a b) (le b c)" то он тебе все равно выведет "a <= b <= c"? Т.е. туда понапихали какую-то логику зажатия питушни в эту вот нотацию? А по какому алгоритму оно в эти нотации зажимает? Я могу эти правила зажатия реальной питушни в нотацию контролировать?
Можно кстати такие нотациионные зожатия и для сишных говномакросов сделать, в какой-нибудь говноIDE. Типа вот наводишь мышкой на какую-то хуйню вида a = b*b*b*b;, и тебе показывает "это можно через говномакрос завернуть в a = POW2(POW2(b)); или в a = POW4(b);"
> Ты хочешь, чтобы тебе кот реверсинженерился в мокросню?
Да, например представим что есть код, в котором очень много повторяющейся хуйни, которую можно свернуть в макросню. Я пишу макросню, а потом каким-то хреном этот код зожимаю в эту макросню, чтоб читабельнее было. Какие-нибудь говноIDE так умеют?
> А фиг знает, я особо не вникала. Первую подходящую, скорее всего. Или по приоритетам которые на них написаны.
Вообще, хуита эти ващи нотации-наняции, декоративная питушня какая-то. То ли дело работа напрямую с AST. А нотации эту работу затрудняют т.к. загораживают собой этот самый AST
Можно сделать препроцессор под такую хуйню - один препроцессор раскрывает нотации в AST, другой пытается этот AST обратно зожать в какие-то нотации по хуй знает каким эвристикам.
А этот макрос без приоритетов как будет "матчить" что-то в духе "a <= b <= c <= d"? А "a <= b <= (c <= d)". Это красиво звучит, но как этот макрос будет разрешать s-s, s-r конфликты? Придется передавать макросу ассоциативность и приоритет. Как-то подозрительно напоминает костыльный генератор парсеров для замены нотаций.
Точно так же можно рассматривать, как в примере с "@N", потому что это то же самое получилось, только "@N" вдруг сам разрешил конфликты между правилами.
> А этот макрос без приоритетов как будет "матчить" что-то в духе "a <= b <= c <= d"?
Никак не матчить. Написать что это ambiguous.
> А "a <= b <= (c <= d)".
Как "(and (<= a b) (<= b (<= c d)) )"
> Это красиво звучит, но как этот макрос будет разрешать s-s, s-r конфликты?
Он будет предлагать расставить скобки, чтобы никаких конфликтов не было. Например, если есть "a + b * c * d + e", это никак не будет матчиться.
Если же "a + ( b * c * d ) + e" то тогда всё четко. Т.е. идем от самых глубоко вложенных скобок, видим "( b * c * d )" - есть какое-то общее правило для заматчивания умножений кучи штук, и это раскрывается в (* b (* c d)) допустим. Потом уровнем выше там "a + (* b (* c d)) + e" и тут срабатывает правило для сложения кучи штук, получаем "(+ a (+ (* b (* c d)) e))"
> Придется передавать макросу ассоциативность и приоритет.
Не нужна ни ассоциативность, ни приоритет. (Примечание: ассоциативность не нужна конкретно на уровне матчера "нотаций-макросов", а вообще нужна и полезна, как свойство для доказательства чего-то. Как впрочем и дистрибутивность. Но ты ж не за то, чтобы тебе нотации a*(b+c) перписывали в (a*b)+(a*c), верно?)
Нет никакого высшего глубокого смысла в том, что в математической записи вида "2 + 2 * 2" надо сначала умножать 2 на 2 и потом прибавлять 2 к получившемуся результату. Ккогда-то давно математики так договорились, что у нас вот будут какие-то там приоритеты, вот и всё. Ничего разумного, доброго, вечного в этом нет.
З.Ы. Вообще в теории можно выгрузить скрипт из coq в ml, загрузить его как плагин и делать что-то с коковскими термами -- пруфы там строить и т.п. Но это изврат, конечно.
if else это просто сахарок для матчинга типов где 2 конструктора. Причём с ним только так ногу отстрелить можно т.к. true это первый из них, а не как-то помеченный.
Это просто синтаксический сахарок для match типов с двумя конструкторами:
Coq < Inductive foo := bar | baz.
foo is defined
foo_rect is defined
foo_ind is defined
foo_rec is defined
foo_sind is defined
Coq < Compute (if bar then 1 else 2).
= 1
: nat
Вот и в документации пишут:
> (IF_then_else P Q R), written IF P then Q else R denotes either P and Q, or ~P and R
> Definition IF_then_else (P Q R:Prop) := P /\ Q \/ ~ P /\ R.
Во валит! Сейчас я наверно глупость скажу
Разные логики. Prop — пропозиция конструктивистской логики, а bool — булевской. Второе можно определить внутри первого.
если очень упростить, то пропы это вселенная типов с определенными свойствами (это как раз конструкция, встроенная в язык). булеан --- один конкретный тип, который можно определить самому(ой)
кста, вдруг вспомнил предыдущий кокосрач, я спросил у коллеги, и он мне скинул папиру, где показано, что CiC и ZFC+недостижимые кардиналы эквипотентны (там чуть более сложная формулировка, потому что там зависимость от конкретной вселенной и конкретного кардинала). называется sets in types, types in sets
Если построить ADT через кодирование Скотта, то match у тебя получится автоматически. Ты вызываешь инстанс ADT, передав ему хендлеры для всех веток и оно диспатчит вызов куда надо. Самое сложное тут -- аккуратно всё это обмазать типами.
øто может привести к проблемам со сложными и нерегулярными структурами данных, кмк. например, гадты из хачкеля будут сплошной болью: нужен мю-кобенатор для типов, равенства внутри, импредикативность временами
Два года назад у чуваков через открытый порт для winbox на микротах увели базу логинов-паролей.
А сегодня по этим паролям к ним зашли, и включили ботнет.
Тут прекрасно всё: и торчащий наружу порт, и аутентификация по паролю в 2021-м году. И это полупрофессиональное оборудование!
На микротах есть ssh с ключом. Там же линукс внутри.
Аунетрифицироваться надо всегда по ключу.
Во-первых его хрен подберешь.
Во-вторых если хакер скоммуниздит базу публичных ключей с устройства, то это не поможет ему подобрать прив[ИНЬЮ_ЗАЕБАЛ_ФИЛЬТР]тный.
В случае пароля конечно тоже не шибко поможет если хеш с солью, наверное
Если хеш без соли, то ты легко найдешь в интеренте хеши поплуряных паролей.
Если с солью, то будешь брутить. Сбрутить ключ нереально. Насколько реально сбрутить пароль с большой солью и sha2 я не знаю, но думаю что тоже очень сложно
Не совсем... Пароль всё-таки порождает желание его побрутить. Вдруг он слабый. В случае с ключом атак тупо не будет т.к. они бессмысленны. Увидев ключ хакер просто уйдёт в другое место.
А почему нельзя скрть информацию есть ли у меня аутентификация по паролю?
Хакер приходит и спрашивает: ты пароли или ключи принимаешь?
Сервер отвечает: иди нахуй
Ну если ты допилишь клиента, чтобы он игнорил "иди нахуй", вай нот?
Но учти, что это security through obscurity т.к. твой сервак всё-таки принимает пароли. И какой-нибудь достаточно тупой бот забудет проверить поддерживаемые способы аутентификации и случайно залогинится, лол.
Ну я и говорю, что твой поинт «если у меня ключ, то хакер пароль не будет перебирать» не всегда верный. А если подпилить протокол, чтобы скрывать эту информацию, то будут перебирать пароли всегда.
Поэтому такая защита от засирания логов пока что оправдана.
Боты знают диапазоны айпишников, на которых могут находиться сервера. IPv4-адресов не так много. Если бы мир перешёл на IPv6, они бы, конечно, занякались искать рабочие айпишники.
Больше половины трафика типичного сервера — это китайские и американские боты, пытающиеся набрутить пароль к SSH.
У моего знакомого админа скриптец скачивает российские адреса с какого-то сервера, и разрешает доступ только с них, потому что ничего хорошего из Индии к нему всё равно не придет
Про диапазоны: «Интернет» разделён на сегменты:
• RIPE — зарубежная Европа и СНГ.
• APNIC — «азиатско-тихоокеанский регион» на муриканском жаргоне — это как раз индусы и китайцы. И Австралия вроде.
• ARIN — североамериканцы.
• LACNIC — латиноамериканцы.
• AFRINIC — африканцы.
Айпишники, принадлежащие этим сегментам, найти очень легко. Для средств администрирования можно оставить RIPE.
Да не особо поможет, как мне кажется. Сетки хостеров и интервал, с которым они раздают подсети, точно так же известны будут, а ты в своей подсети вряд ли будешь брать рандомный айпишник из середины. То на то и выйдет.
Да, в качестве первой линии обороны неплохо. Чел снаружи, даже если и будет знать о такой технологии, то всё равно не узнает, угадал ли он кобенацию портов.
С натом — смотря как нат устроен: если он выделяет по порту на каждое логическое соединение — то никак, да; а если он жадный и просто маппит source port клиента в случайный (но фиксированный в рамках сессии) внешний source port — то всё будет работать как и без ната.
Нок-прокси — отличная идея. С ним можно сделать автонокинг: делаешь «ssh root@127.0.0.1:1234», подключение хватает процесс прокси, стучится по заданным в конфиге портам, и только после этого проксирует трафик на удалённый сервер.
А вообще ты прав, да: если NAT тупой и будет открывать новое соединение (с новым внешним source port) на каждый пакетик — то да, мы соснём. Тут разве что эвристики помогут (типа с какого source port первый раз после нока подключились — тому и открываем, а остальным хуй).
Не выбор, а фиксация.
Серверу приходит правильная последовательность с 1.2.3.4:1234, где 1.2.3.4 — внешний IP ната, 1234 — случайно выбранный натом source port. Сервер открывает заветный 22 только для 1.2.3.4:1234. Клиент, которому нат выделил этот порт, радуется, остальные занатовцы зайти не могут.
Не просто не передается, а каждая строка выполняется в отдельном шеле!
Так что если ты хочешь их объеденить, то нужно писать "cd /foo && petuh" например.
Такая загадка мне по нраву, ведь я ещё новенький, поэтому многого не знаю.
Потому что у автора "make-файла" случился внезапный приступ эпилепсии, и он посреди ввода путя нажал "return", точку и слеш и вместо "cd /opt/petuh/petuh" написал XYNTY?
Кстати, я еще ни разу не читал мейкфайлы: если они не работают, я просто охуеваю и устанавливаю что-нибудь другое.
j123123 # 0
j123123 # 0 ⇈
Или NOR: https://en.wikipedia.org/wiki/NOR_logic
bormand # 0 ⇈
Поэтому в булеанах нет ничего специального, можешь сам такие же запилить.
j123123 # 0 ⇈
bormand # 0 ⇈
А так -- да, ML'ка по синтаксису. OCaml, емнип, вообще пилили специально чтобы петуха на нём писать.
j123123 # 0 ⇈
А зачем делать такой сложный базис? В "Metamath" базис намного проще.
Почему Coq не сделали с гомоиконностью?
bormand # 0 ⇈
Из-за этого минималистичный CoC (calculus of constructions) превратился в раздутый CIC (calculus of inductive constructions).
JloJle4Ka # 0 ⇈
Разговаривать словечки
Выясняли кто умней
У кого матан сложней!
bormand # 0 ⇈
Х.з., видимо нотации показались более удобными. Они и при отладочном выводе работают в обратную сторону, в отличие от универсальных гомоикон. Ну и на ядро никак не влияют.
А ltac тьюринг полный, что в ядро тащить вообще нельзя.
j123123 # 0 ⇈
А почему они показались более удобными? Тут наверное причина только в том, что люди, запиливавшие Coq, были ML-еблюбами
bormand # 0 ⇈
Фиг знает, потому что это чисто синтаксическое преобразование без всяких подводных камней?
j123123 # 0 ⇈
bormand # 0 ⇈
На s-выражениях такая фича выглядела бы как макрос с дословной подстановкой аргументов без какой-либо обработки данных.
j123123 # 0 ⇈
Да, это называется "макрос".
> На s-выражениях такая фича выглядела бы как макрос с дословной подстановкой аргументов без какой-либо обработки данных.
И в чем проблема?
В общем моя твоя не понимать
bormand # 0 ⇈
Т.е. если "нотация" -- это "макрос", то очень-очень ограниченный.
j123123 # 0 ⇈
Можно даже сделать специальный макрос, который принимает макрос в качестве аргумента и убеджается в том, что этот макрос соответствует некоторым критериям, и вот только тогда он в что-то раскрывается. А иначе ошибка компиляции.
Не вижу проблемы короче. Вот если б наоборот, макросы были более ограничеными...
Hijikata # 0 ⇈
j123123 # 0 ⇈
CHayT # 0 ⇈
guest # 0 ⇈
Hijikata # 0 ⇈
j123123 # 0 ⇈
А сама гомоиконичность это не только про макросы, а и про удобство работы с AST.
https://archive.jlongster.com/Lisp--It-s-Not-About-Macros,-It-s-About-Read
Собственно:
> Once you understand that Lisp code is data (lists of atoms), you realize that you can use read to read in Lisp code as data. And since Lisp comes with a set of functions for elegantly processing lists, suddenly it's really easy to parse Lisp code.
> You just wrote a parser that turns all define expressions into lambda expressions.
> That should impress you. How would you do that in Python? Or Javascript? You need access to the AST and need to learn all the internal methods for parsing it. Lisp code is an AST.
Т.е. профит тут в синтаксиальной однородности, что можно легко генерить и легко читать эту хрень, не думая при чтении/генерации о всякой срани типа "Precedence" и "Associativity" как в https://coq.inria.fr/refman/language/coq-library.html#init-notations
Hijikata # 0 ⇈
j123123 # 0 ⇈
А суть не в макросах, а в однородном синтаксисе. Полноценные макросы могут тоже присутствовать, только они могут раскрываться как какой-нибудь сишный препроцессор, и потом уже над "раскрытым" представлением можно делать какие-то манипуляции.
Зачем однородный синтаксис? Чтобы удобно конструировать и читать это всё, чтобы можно было удобно это в что-то другое экспортнуть. Чтобы не держать в голове правила приоритетов каких-то операций, и что какая-то там функция может быть размазана на несколько "инфиксных операций". Вот например https://coq.inria.fr/refman/language/coq-library.html#init-notations
Тут есть такая штука "_ <= _ <= _" напоминающая какой-то японский смайлик. А по-сути эта функция от трех аргументов, которая про "(a <= b) && (b <= c)" А в каком-нибудь лиспе это можно записать как (and (<= a b) (<= b c)) и это дерево.
И я допустим могу по этому дереву ходить какими-то "итераторами" и что-то в нем добавлять/переставлять, это просто и понятно. А зачем это делать через два инфиксных оператора? И еще приоритеты какие-то? Зачем? Зачем?
j123123 # 0 ⇈
j123123 # 0 ⇈
Но проблемы с приоритетом операций тут не будет, и такой макрос до раскрытия тоже можно рассматривать как дерево
А как мне рассматривать "как дерево" эти нотации с приоритетами?
JloJle4Ka # 0 ⇈
CHayT # 0 ⇈
bormand # 0 ⇈
Просто для удобства пользователя эта штука вводится и выводится как a <= b <= c.
Не нравятся нотации? Выруби их в переменной или галочкой в IDE. Будешь читать портянки говна именно так, как их видит прувер.
Правда вместо чисел у тебя будут S (S (S (S O)))). Но это ведь мелочи...
guest # 0 ⇈
https://youtube.com/watch?v=TJKgq_DcJCw
j123123 # 0 ⇈
А почему б пруверу сами эти нотации не видеть как дерево, и не оттранслировать теоремы-леммы в теоремы-леммы в терминах этой другой нотации? Например, если мне надо что-то доказать, что завязано на десятичную систему счисления, ну скажем https://ru.wikipedia.org/wiki/Проблема_196
и вот я описываю правила отображения S (S (S ... в какой-то там (DEC 1 9 6), и этот S ( S ( S ... может сложиться в этот DEC и наоборот. И описываю теорему про (DEC 1 9 6) и пруваю в терминах этой же нотации
> Правда вместо чисел у тебя будут S (S (S (S O)))). Но это ведь мелочи...
А обязательно ли числа "хранить" такой питушней в представлении для прувера? Можно ж как-нибудь
Ну и какая-то питушня может биективно отобразить (DEC 1 1) в (S (S (S (S (S (S (S (S (S (S O)))))))))) и наоборот.
bormand # 0 ⇈
Нет, но эта форма очень удобна для индуктивных пруфов.
j123123 # 0 ⇈
А если у тебя какое-то очень большое число, которое в S (S (S (S ... форме не будет помещаться в оперативной памяти? Например, если ты захочешь взять самое большое число, для которого доказана его простота, и захочешь это проверить в Coq, как ты с этим числом будешь работать?
Например https://ru.wikipedia.org/wiki/Наибольшее_известное_простое_число
А если это будет простое число, которое числом Мерсенна не является?
bormand # 0 ⇈
Ну тут скорее я буду доказывать, что мой тест простоты в общем виде соответствует спеке.
А потом уже выгружать код из петуха и гонять его на твоём числе.
А для доказательств в общем виде большие числа обычно не нужны.
j123123 # 0 ⇈
Мне в нотациях не нравится, что там какие-то "приоритеты" и "ассоциативность" есть, которые надо иметь в виду для понимания смысла. Можно сделать нотации на макросне, где ничего такого нет. Вот вместо "a <= b <= c" сделать "(@N a <= b <= c)" - и нету никаких проблем с ассоциативностью. Если надо записать "a <= b <= c + d" то просто пишешь "(@N a <= b <= (@N c + d))" и нет никаких неоднозначностей.
И эту макросню точно так же можно зажимать и разжимать
CHayT # 0 ⇈
j123123 # 0 ⇈
CHayT # 0 ⇈
Hijikata # 0 ⇈
CHayT # 0 ⇈
j123123 # 0 ⇈
CHayT # 0 ⇈
j123123 # 0 ⇈
bormand # 0 ⇈
Дык всё просто...
Я пишу a <= b <= c. Петух это видит как and (le a b) (le b c), но выводит мне как a <= b <= c.
Я пишу remember (a <= b) as d. Петух видит результат этой замены как and d (le b c), но выводит мне d /\ b <= c.
j123123 # 0 ⇈
А если ты напишешь "and (le a b) (le b c)" то он тебе все равно выведет "a <= b <= c"? Т.е. туда понапихали какую-то логику зажатия питушни в эту вот нотацию? А по какому алгоритму оно в эти нотации зажимает? Я могу эти правила зажатия реальной питушни в нотацию контролировать?
bormand # 0 ⇈
Именно так.
> А по какому алгоритму оно в эти нотации зажимает?
А фиг знает, я особо не вникала. Первую подходящую, скорее всего. Или по приоритетам которые на них написаны.
Ты пишешь что-то в духе Notation "a <= b <= c" := and (le a b) (le b c) чтобы ввести новую нотацию. И она начинает в обе стороны работать.
j123123 # 0 ⇈
bormand # 0 ⇈
В сишке некоторые макросы необратимы (конкатенация, стрингификация).
j123123 # 0 ⇈
bormand # 0 ⇈
ObeseYoung # 0 ⇈
И, кстати, почему для asciiz-строк puts, а не putz?
j123123 # 0 ⇈
Да, например представим что есть код, в котором очень много повторяющейся хуйни, которую можно свернуть в макросню. Я пишу макросню, а потом каким-то хреном этот код зожимаю в эту макросню, чтоб читабельнее было. Какие-нибудь говноIDE так умеют?
ObeseYoung # 0 ⇈
Это будет дорогостильноIDE томущо задача нетривиальная
j123123 # 0 ⇈
JloJle4Ka # 0 ⇈
j123123 # 0 ⇈
Лучше уж сразу pituz
j123123 # 0 ⇈
Вообще, хуита эти ващи нотации-наняции, декоративная питушня какая-то. То ли дело работа напрямую с AST. А нотации эту работу затрудняют т.к. загораживают собой этот самый AST
Можно сделать препроцессор под такую хуйню - один препроцессор раскрывает нотации в AST, другой пытается этот AST обратно зожать в какие-то нотации по хуй знает каким эвристикам.
j123123 # 0 ⇈
Hijikata # 0 ⇈
Точно так же можно рассматривать, как в примере с "@N", потому что это то же самое получилось, только "@N" вдруг сам разрешил конфликты между правилами.
j123123 # 0 ⇈
Никак не матчить. Написать что это ambiguous.
> А "a <= b <= (c <= d)".
Как "(and (<= a b) (<= b (<= c d)) )"
> Это красиво звучит, но как этот макрос будет разрешать s-s, s-r конфликты?
Он будет предлагать расставить скобки, чтобы никаких конфликтов не было. Например, если есть "a + b * c * d + e", это никак не будет матчиться.
Если же "a + ( b * c * d ) + e" то тогда всё четко. Т.е. идем от самых глубоко вложенных скобок, видим "( b * c * d )" - есть какое-то общее правило для заматчивания умножений кучи штук, и это раскрывается в (* b (* c d)) допустим. Потом уровнем выше там "a + (* b (* c d)) + e" и тут срабатывает правило для сложения кучи штук, получаем "(+ a (+ (* b (* c d)) e))"
> Придется передавать макросу ассоциативность и приоритет.
Не нужна ни ассоциативность, ни приоритет. (Примечание: ассоциативность не нужна конкретно на уровне матчера "нотаций-макросов", а вообще нужна и полезна, как свойство для доказательства чего-то. Как впрочем и дистрибутивность. Но ты ж не за то, чтобы тебе нотации a*(b+c) перписывали в (a*b)+(a*c), верно?)
Нет никакого высшего глубокого смысла в том, что в математической записи вида "2 + 2 * 2" надо сначала умножать 2 на 2 и потом прибавлять 2 к получившемуся результату. Ккогда-то давно математики так договорились, что у нас вот будут какие-то там приоритеты, вот и всё. Ничего разумного, доброго, вечного в этом нет.
И вообще, надо чтоб префиксная нотация
CHayT # 0 ⇈
Тебе нужна ЙАЖА:
1) Инфиксные операторы перегружать нельзя, и пользоваться ими нельзя.
2) Не надо думать ни про какие приоритеты.
Идеальный язык!
j123123 # 0 ⇈
Не, я скорее за LISP и FORTH в этом плане. А жаба говно, там даже беззнакового int не сделали.
guest # 0 ⇈
Любишь беззнаковый size_t в с++?
3_dar # 0 ⇈
j123123 # 0 ⇈
bormand # 0 ⇈
guest # 0 ⇈
bormand # 0
CEHT9I6PbCKuu_nemyx # 0
Так же можно организовать ленивость для логических операций в любом ЯП.
ASD_77 # 0
bormand # 0 ⇈
JloJle4Ka # 0 ⇈
«Хипстеры, хипстеры, эти хипстера – и у них откуда-то денег дохера».
CHayT # 0 ⇈
3.14159265 # 0 ⇈
Минимализм это хорошо. Проще реализовывать язык.
Средствами языка можно описывать сложные конструкты..
Другой вопрос как реализовали сам if ... then ... else ...
CHayT # 0 ⇈
3.14159265 # 0 ⇈
> синтаксический сахарок для match типов
А match тоже собирают из чего-то более примитивного?
CHayT # 0 ⇈
Нет, это полностью аналогично haskell'ному
CHayT # 0 ⇈
3.14159265 # 0 ⇈
Логическая импликация.
Вот и в документации пишут:
> (IF_then_else P Q R), written IF P then Q else R denotes either P and Q, or ~P and R
> Definition IF_then_else (P Q R:Prop) := P /\ Q \/ ~ P /\ R.
CHayT # 0 ⇈
3.14159265 # 0 ⇈
bormand # 0 ⇈
Второй просто предикат для рассуждений.
CHayT # 0 ⇈
Разные логики. Prop — пропозиция конструктивистской логики, а bool — булевской. Второе можно определить внутри первого.
Hijikata # 0 ⇈
ObeseYoung # 0 ⇈
Hijikata # 0 ⇈
j123123 # 0 ⇈
Hijikata # 0 ⇈
ISO # 0 ⇈
Фу, анскилл. Как на этом сделать логику без анскильного tertium non datur?
CHayT # 0 ⇈
bormand # 0 ⇈
Можно на чистом лямбда-исчислении замутить.
CHayT # 0 ⇈
bormand # 0 ⇈
Видимо по-другому сложно ограничить рекурсию?
CHayT # 0 ⇈
bormand # 0 ⇈
Hijikata # 0 ⇈
CHayT # 0 ⇈
Нет, насколько я знаю, он часть формальной системы.
j123123 # 0 ⇈
Как тернарный оператор в сишке наверное
В языке SMTLib для этого есть "ite"
guest # 0
JloJle4Ka # 0 ⇈
guest # 0 ⇈
Например вот: https://blog.mikrotik.com/security/meris-botnet.html
Два года назад у чуваков через открытый порт для winbox на микротах увели базу логинов-паролей.
А сегодня по этим паролям к ним зашли, и включили ботнет.
Тут прекрасно всё: и торчащий наружу порт, и аутентификация по паролю в 2021-м году. И это полупрофессиональное оборудование!
JloJle4Ka # 0 ⇈
> и аутентификация по паролю в 2021-м году
А как надо?
bormand # 0 ⇈
guest # 0 ⇈
guest # 0 ⇈
guest # 0 ⇈
Аунетрифицироваться надо всегда по ключу.
Во-первых его хрен подберешь.
Во-вторых если хакер скоммуниздит базу публичных ключей с устройства, то это не поможет ему подобрать прив[ИНЬЮ_ЗАЕБАЛ_ФИЛЬТР]тный.
В случае пароля конечно тоже не шибко поможет если хеш с солью, наверное
guest # 0 ⇈
guest # 0 ⇈
А ключ это асиметричное шифрование. Привтный ключ только у меня есть, а на сервере от него публичный.
Если ты взломал сервер, то ты можешь оттуда получить только публичные ключи пользователей, но не привтные
guest # 0 ⇈
guest # 0 ⇈
Если с солью, то будешь брутить. Сбрутить ключ нереально. Насколько реально сбрутить пароль с большой солью и sha2 я не знаю, но думаю что тоже очень сложно
guest # 0 ⇈
bormand # 0 ⇈
guest # 0 ⇈
Хакер приходит и спрашивает: ты пароли или ключи принимаешь?
Сервер отвечает: иди нахуй
bormand # 0 ⇈
Но учти, что это security through obscurity т.к. твой сервак всё-таки принимает пароли. И какой-нибудь достаточно тупой бот забудет проверить поддерживаемые способы аутентификации и случайно залогинится, лол.
guest # 0 ⇈
Ну так а я о чём? ))
> Увидев ключ хакер просто уйдёт в другое место
А на самом деле сервак может принимать пароли тоже
bormand # 0 ⇈
guest # 0 ⇈
Поэтому такая защита от засирания логов пока что оправдана.
guest # 0 ⇈
guest # 0 ⇈
Обычно в протоколах клиент и сервер договариваются о способоах аутентификации
guest # 0 ⇈
Правда хороший пароль еще хрен сделаешь, а ключ хорош сам по себе.
А еще всякие ботнеты обычно не брутят ключи, бо бессмысленно.
Если включить аунтентификацию по паролю, то будут постоянно лезть "admin pa$$w0rd"
JloJle4Ka # 0 ⇈
А если про сервер не рассказывать на говнокоде?
bormand # 0 ⇈
guest # 0 ⇈
Если унесешь порт с 22 куда-то за эвфемерные порты типа 50123, то будут срать чуть меньше.
Если настроишь SSHGuard, то еще меньше будут срать.
Но всё равно найдут, и будут брутить.
RDP и SSH всегда брутят
CEHT9I6PbCKuu_nemyx # 0 ⇈
Больше половины трафика типичного сервера — это китайские и американские боты, пытающиеся набрутить пароль к SSH.
guest # 0 ⇈
guest # 0 ⇈
guest # 0 ⇈
CEHT9I6PbCKuu_nemyx # 0 ⇈
Про диапазоны: «Интернет» разделён на сегменты:
• RIPE — зарубежная Европа и СНГ.
• APNIC — «азиатско-тихоокеанский регион» на муриканском жаргоне — это как раз индусы и китайцы. И Австралия вроде.
• ARIN — североамериканцы.
• LACNIC — латиноамериканцы.
• AFRINIC — африканцы.
Айпишники, принадлежащие этим сегментам, найти очень легко. Для средств администрирования можно оставить RIPE.
guest # 0 ⇈
guest # 0 ⇈
Вот пускай лучше эту дыру ковыряют десять ботов из Европы чем десять миллионов ботов из КНР, Индии и Африки.
Это не только ssh касается, но и вообще любого сервиса
CEHT9I6PbCKuu_nemyx # 0 ⇈
guest # 0 ⇈
ну в общем старое админское правило "чем меньше всего можно -- тем лучше"
ObeseYoung # 0 ⇈
guest # 0 ⇈
А логины тоже брутят?
guest # 0 ⇈
guest # 0 ⇈
bormand # 0 ⇈
Да не особо поможет, как мне кажется. Сетки хостеров и интервал, с которым они раздают подсети, точно так же известны будут, а ты в своей подсети вряд ли будешь брать рандомный айпишник из середины. То на то и выйдет.
CEHT9I6PbCKuu_nemyx # 0 ⇈
CHayT # 0 ⇈
guest # 0 ⇈
Хорошо, да. Но одного этого мало, так как ты можешь оказаться за каким-то глубоким NATом, и нок откроется для всей сети
CEHT9I6PbCKuu_nemyx # 0 ⇈
Особенно круто, когда постучал из «жопореза», в котором на одном айпишнике сорок тысяч обезьян.
guest # 0 ⇈
Вот ты должен послать в порт 1234 пакет, я его дропну
Затем в порт 4234, я его тоже дропну
И только тогда я открою 22
Чел снаружи даже не догадается вообеще что тут что-то есть
CEHT9I6PbCKuu_nemyx # 0 ⇈
ObeseYoung # 0 ⇈
Какие обскурити )))
ISO # 0 ⇈
Так надо открывать для одного source port.
guest # 0 ⇈
ISO # 0 ⇈
bormand # 0 ⇈
guest # 0 ⇈
Выбирать его самому при подключении что ли?
Если порт тебе назначит операционка, то на каждый сокет будет свой порт
Или вы хотите как-то переиспользовать сокет из которого стучитесь?
ISO # 0 ⇈
С натом — смотря как нат устроен: если он выделяет по порту на каждое логическое соединение — то никак, да; а если он жадный и просто маппит source port клиента в случайный (но фиксированный в рамках сессии) внешний source port — то всё будет работать как и без ната.
guest # 0 ⇈
Но в общем случае какой-нить тупой клиент этого не умеет, а если я попрошу пользователя стукнуться телнетом или браузером, то ничего не сработает.
А значит нужно нужно или делать умный клиент, или реализовывать нокающий прокси
Вполне возможно, такой у knockd уже и есть
ISO # 0 ⇈
guest # 0 ⇈
Если нет, надо написать :))
ISO # 0 ⇈
ISO # 0 ⇈
CEHT9I6PbCKuu_nemyx # 0 ⇈
ISO # 0 ⇈
Серверу приходит правильная последовательность с 1.2.3.4:1234, где 1.2.3.4 — внешний IP ната, 1234 — случайно выбранный натом source port. Сервер открывает заветный 22 только для 1.2.3.4:1234. Клиент, которому нат выделил этот порт, радуется, остальные занатовцы зайти не могут.
ObeseYoung # 0 ⇈
https://www.cisco.com/c/en/us/support/docs/security-vpn/lock-key/7604-13.html
guest # 0 ⇈
Дан Makefile
Известно, что ``/opt/petuh/petuh`` существует, и доступен для запуска. Однако же файл не работает ни из какой папки, кроме ``/opt/petuh``.
В чем дело?
bormand # 0 ⇈
Окружение между строчками мейкфайла не передаётся?
guest # 0 ⇈
Так что если ты хочешь их объеденить, то нужно писать "cd /foo && petuh" например.
Это бывает неожиданно
guest # 0 ⇈
> Однако же файл не работает ни из какой папки, кроме `/opt/petuh`.
То есть cd /opt && ./petuh/petuh всё таки будет работать?
guest # 0 ⇈
под "файл" я имел ввиду Makefile
guest # 0 ⇈
CHayT # 0 ⇈
guest # 0 ⇈
Представляете как удобно писать цикл for, например?
Выглядит как макрос
JloJle4Ka # 0 ⇈
Потому что у автора "make-файла" случился внезапный приступ эпилепсии, и он посреди ввода путя нажал "return", точку и слеш и вместо "cd /opt/petuh/petuh" написал XYNTY?
Кстати, я еще ни разу не читал мейкфайлы: если они не работают, я просто охуеваю и устанавливаю что-нибудь другое.
guest # 0
guest # 0
ObeseYoung # 0 ⇈