так при этом проверяется только что ничего по памяти не проедет там где не надо

будет ли программист при этом какую-то более интересную спецификацию проверять - это уже другой вопрос

Смысл в том, что функции языка у тебя объекты первого поряда в нём же, как в системе доказательства теорем. А если ты будешь питон на coq верифицировать, то тебе нужно будет работать с программой как со сомнительными данными какого-то странного индуктивного типа синтаксических структур питона

будет ли программист при этом какую-то более интересную спецификацию проверять - это уже другой вопрос

Ну, это уже задача блокчейна цели ставить

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

Если вы про верификацию смарт-контрактов, то это тупо проверка что этот код компилится с этой версией компилятора в этот байткод

Сейчас этим занимается только сайт etherscan

Если вы про верификацию смарт-контрактов, то это тупо проверка что этот код компилится с этой версией компилятора в этот байткод

Ну такое

но минимальная спецификация которую придется верифицировать если писать на тотальном языке - не очень интересная

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

Берёшь Ada Spark и на ней пишешь. Получается верифицировано, и Coq учить не надо.

Хочется чтобы были математические гарантии на финансовые инструменты

О да - год назад моя почта разрывалась от таких. Напишите нам проект и смарт и проведите IСO выведите на биржи, а мы вам токенов наших будующих отсыпем процетов Х)))

у меня что-то похожее )

Хочется чтобы были математические гарантии на финансовые инструменты

Ну мне нет, финансовые инструменты должны гореть в аду, но рынку да

Берёшь Ada Spark и на ней пишешь. Получается верифицировано, и Coq учить не надо.

А в чем там верификация, там же просто контракты расставляются на уровне ассертов?

А в чем там верификация, там же просто контракты расставляются на уровне ассертов?

Эти контракты сверяются с кодом статически.

Эти контракты сверяются с кодом статически.

А какая разница статически или в рантайме. Код работает по контракту или не работает, в этом же кайф?

А какая разница статически или в рантайме. Код работает по контракту или не работает, в этом же кайф?

https://xakep.ru/2018/02/27/smart-contracts-problems/

А какая разница статически или в рантайме. Код работает по контракту или не работает, в этом же кайф?

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

Парити это кстати ребята, пишушие на расте

Это боянистая история с их багом, руки отрубать таким контрактописателям

https://xakep.ru/2018/02/27/smart-contracts-problems/

Чо за баг я так и не понял из статьи

В эфири проблемы нету, проблема в кадрах как всегда

А какая разница статически или в рантайме. Код работает по контракту или не работает, в этом же кайф?

Мне кажется, у нас разное понимание того, что такое верификация. Контракт - это декларации, что должен делать код, и чего не должен. Декларация краткая и понятная, а код может замысловато грызть байты. Верификатор проверяет соответствие кода декларациям, и делает это не в райнтайме, а до того.

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

И удалить всё нахер

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

ну падажи, ну то что упадет ПО это не приятно, но не так неприятно для бизнеса как выполнение говна?

Selfdestruct

Нефиг писать такие сложные контракты, если честно

ну падажи, ну то что упадет ПО это не приятно, но не так неприятно для бизнеса как выполнение говна?

отсутствие падений и говна проверяется одинаково

Мне странно что криптокотов

Не сломали

Ведь там 2000+ строк кода

В эфири проблемы нету, проблема в кадрах как всегда

> как всегда вот именно поэтому нужно как можно сильнее ослабить влияние самой ненадёжной части системы - человека, заставляя его верефицировать автоматическими средствами смартконтракты

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

как если это проверка?

Не сломали

Криптовалерьянкой

как если это проверка?

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

https://blog.zeppelin.solutions/on-the-parity-wallet-multisig-hack-405a8c12e8f7

А, тут путаница в терминах контракт и смарт контракт

смысл в том что перемудрили с логикой и не закрыли очевидную дыру

я не очень шарю в последних тенденциях, но это все ещё про Haskell?

а нет, сорян, это про днугой хак

Вот https://blog.springrole.com/parity-multi-sig-wallets-funds-frozen-explained-768ac072763c

В парити так сильно впечатлились этими своими "хаками", что начали всерьез работать над тем, чтобы уйти от Solidity и EVM к чему-то, что компилится в WebAssembly. Хотя по-моему это тупик, и просто более ответственных людей надо брать на смарт-контракты

я не очень шарю в последних тенденциях, но это все ещё про Haskell?

Это из расточата набег (судя по обсуждению)

а не JS макак

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

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

с этим как раз все норм, ведь этот код будет крутиться потом на каждой машине, кототрая будет этот контракт проверять

тут уже не до чистоты и reasoning'а

с этим как раз все норм, ведь этот код будет крутиться потом на каждой машине, кототрая будет этот контракт проверять

В блокчейн-мире всё как у Жарова: "Поэтому, если выбирать между комфортом и безопасностью, я выбираю безопасность"

В блокчейн-мире всё как у Жарова: "Поэтому, если выбирать между комфортом и безопасностью, я выбираю безопасность"

...не заслуживает ни того, ни другого

никто не хочет переложить ethereum yellow paper на хаскель?

это что за соцсеточка?

я вот сижу думаю как бы провернуть эту штуку, свой эфир

это что за соцсеточка?

ResearchGate

...не заслуживает ни того, ни другого

Классический аналог мира блокчейна вообще живёт на мейнфреймах и коболе.

в двух словах все в этой бумажке

никто не хочет переложить ethereum yellow paper на хаскель?

IOHK вроде бы этим и занимается

но к сожалению не всё, куски документации разбросаны по всему интернету

Поприветствуем HR

Say blockchain once again, motherfucker. I dare you! I double dare you!

ERROR: S client not available

IOHK вроде бы этим и занимается

интересно, спасибо

Тут в соседнем чате го-вакансий два эйчара сцепились.

у метро по объявлению "работа для вас"

здесь

откровенно спамная формулировка

никто не хочет переложить ethereum yellow paper на хаскель?

http://hackage.haskell.org/package/ethereum-client-haskell

http://hackage.haskell.org/package/ethereum-client-haskell

это я видел, оно заброшено

всяко уже есть реализация

всяко уже есть реализация

если только одним глазком. версия от 2015 года

Кого ищете и на какие вакансии?

Тут в соседнем чате го-вакансий два эйчара сцепились.

Рвут гошников на части?

Кого ищете и на какие вакансии?

очевидно, не хаскелистов

очевидно, не хаскелистов

неочевидно, но очень вероятно

Все хаскель-работодатели здесь представлены хотя бы сотрудниками

Тут в соседнем чате го-вакансий два эйчара сцепились.

Дай ссылку на сцепление посмотреть ;)

Все хаскель-работодатели здесь представлены хотя бы сотрудниками

бывают внешние рекрутёры

офтоп

Все хаскель-работодатели здесь представлены хотя бы сотрудниками

ну мало ли, вдруг там можно писать на чём хочешь

Пайтон и ПХП. только Хаскель, Идрис и Coq.

а здесь это зачем?

и окамл.

Предлагаю это стереть

Пайтон и ПХП. только Хаскель, Идрис и Coq.

А руст?

у руста свой чатик же есть

а здесь это зачем?

неужили ты чего-то большего ожидал от очередного рекрутёра?

у руста свой чатик же есть

чатик хаскела захвачен рустерами

у руста свой чатик же есть

У идриса тож

Я думаю и у окамла есть

у окамла совмещенный с ризоном

@dinadzho, если нужны будут хаскелисты, приходите. питон и пхп здесь не комильфо