RR
Прототипировать надо на лиспе, а потом из лиспа генерить хаскель
Size: a a a
2018 March 30
VM
Прототипировать надо на лиспе, а потом из лиспа генерить хаскель
Зачем?
IZ
Почему бы и нет?
IZ
Я бы просто второй этап отбросил, но....
VM
Генерить хаскель?
DR
и щас сижу разбираюсь с Coq — хочу формализовать язык запросов и его трансляцию в SQL
Можем взять к нам разработать, к слову, если надо
RR
Я бы просто второй этап отбросил, но....
поддерживаю
IT
Надо идти до конца, и первый тоже отбросить.
AL
Приветы! Могу рассказать про формализацию относительно примитивных смарт контрактов на coq. Со стейт монадами и доказательствами всего:)
AB
λO
Присоединяюсь к вопросу
λO
λO
Во че нашел
DR
Приветы! Могу рассказать про формализацию относительно примитивных смарт контрактов на coq. Со стейт монадами и доказательствами всего:)
Я начинал кстати такое VM вменяемую для смарт-контрактов на coq прототипировать, но меня тогда остановил зачастую тот факт, что для того, чтобы верификация смысл имела, нужно иметь хорошую формализацию самого блокчейна и операций в нем. Без привязки к этому смысла в этом вижу сильно меньше.
AL
Я начинал кстати такое VM вменяемую для смарт-контрактов на coq прототипировать, но меня тогда остановил зачастую тот факт, что для того, чтобы верификация смысл имела, нужно иметь хорошую формализацию самого блокчейна и операций в нем. Без привязки к этому смысла в этом вижу сильно меньше.
Ну VM в некотором смысле данность до лучших времён, а некоторые факты относительно самих контрактов тоже можно выводить и верифицировать, по крайней мере чтобы обезопасить себя от явных багов. Потом формализация блокчейна, правда без криптографии есть какаято, да и с ней тоже были попытки вполне удачные в свое время
DR
Ну VM в некотором смысле данность до лучших времён, а некоторые факты относительно самих контрактов тоже можно выводить и верифицировать, по крайней мере чтобы обезопасить себя от явных багов. Потом формализация блокчейна, правда без криптографии есть какаято, да и с ней тоже были попытки вполне удачные в свое время
Ну почему же данность. Это только если принять что только EVM существует. К счастью люди этого не принимают и кучу других решений делают.
AL
Ну почему же данность. Это только если принять что только EVM существует. К счастью люди этого не принимают и кучу других решений делают.
Это правда конечно, но имхо во многом вопрос популярности, нежели чем технологии. Я далеко не фанат EVM, скорее наоборот, но дискурс скорее вокруг него пока