Idris 2

Idris is a programming language designed to encourage Type-Driven Development.

In type-driven development, types are tools for constructing programs. We treat the type as the plan for a program, and use the compiler and type checker as our assistant, guiding us to a complete program that satisfies the type. The more expressive the type is that we give up front, the more confidence we can have that the resulting program will be correct.

Я слыхал про Test-driven development (TDD), но зачем нужен type-driven development и что оно в сравнении с ClojureScript — очень приятсвенным диалектом LISP, при этом не отсвечивавшим в последние 5 лет.

Почему я вообще спросил про Idris? — потому, что Idris 2 упоминается, как новая фича в Fedora 43 Beta.

Здравствуйте, Артём, Вы писали:

Аё>Я слыхал про Test-driven development (TDD), но зачем нужен type-driven development и что оно в сравнении с ClojureScript — очень приятсвенным диалектом LISP, при этом не отсвечивавшим в последние 5 лет.

Так вроде примеры неплохо гуглятся Idris-подобные языки позволяют описывать зависимые типы (завтипы по-русски) и проверять их целостность на этапе компиляции. Завтипы это типы данных, зависящие от данных Например, не просто "строка", а "строка-палиндром".

Аё>Почему я вообще спросил про Idris? — потому, что Idris 2 упоминается, как новая фича в Fedora 43 Beta.

Почитал. Старнный проект, который в Release notes упоминает какие пакеты получат обновление, причём, только какие-то выборочные. А все остальные останутся в старой версии? Или они не заслуживают упоминания? Последний раз, когда я изучал Idris, я набрёл на доволно прошаренного чела, который сказал, что Idris полон багов и готов к боевому использованию чуть менее чем никак, и я ему верю.

Здравствуйте, Артём, Вы писали:

Аё>Почему я вообще спросил про Idris? — потому, что Idris 2 упоминается, как новая фича в Fedora 43 Beta.

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

К чему это привело:
https://en.wikipedia.org/wiki/2024_global_telecommunications_hack
https://www.reuters.com/business/media-telecom/chinese-hack-us-telecoms-compromised-more-firms-than-previously-known-wsj-says-2025-01-05/

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

По поводу багов в Идрисе — я в первый же день работы FSharp разработчиком наткнулся на баг в компиляторе, зарепортил его. Что там есть баги — я вполне верю. В C/C++ их было ещё больше (а скорее всего и сейчас есть), но силами миллионов обезьян это всё было выловлено. В Хаскеле тоже имеются баги. Поэтому писать будут на ElectronJS — уж там-то точно нет багов!

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

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

Здравствуйте, koenig, Вы писали:

K>доказуемый код индустрии не по зубам. цена у него запредельная. ок, кругом жадные капиталисты которые гадят тебе в борщ, но в пет проджектах то же самое — в них тоже доказуемого кода нет.

Что такое "доказуемый код"?

Например, в типизированных/типобезопастых языках, проверка типов не гарантирует отсутствие багов. Но, в сравнении с динамическими, по крайней мере там компилятор помогает отлавливать глупые ошибки- когда в одном месте поменял, а в другом забыл.
Чем помогает "доказуемый код"?

Аё>Чем помогает "доказуемый код"?

примерно так
https://en.wikipedia.org/wiki/L4_microkernel_family#High_assurance:_seL4


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

Здравствуйте, cppguard, Вы писали:

C>Так вроде примеры неплохо гуглятся Idris-подобные языки позволяют описывать зависимые типы (завтипы по-русски) и проверять их целостность на этапе компиляции. Завтипы это типы данных, зависящие от данных Например, не просто "строка", а "строка-палиндром".

А не получится ли так, что мы вместо одной программы будем писать две, сравнимого размера? Одна будет в рантайме чего-то делать, другая будет во время компиляции проверять, что первая деляет всё правильно.

Здравствуйте, Артём, Вы писали:

Аё>Что такое "доказуемый код"?

Доказуемый код, это код, который (1) имеет формальную спецификацию того, что он должен делать (2) имеется математическое доказательство того, что код соответствует спецификации.

Вопрос о корректности самой спецификации остаётся за скобками.

Аё>Чем помогает "доказуемый код"?

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

С>Есть такие люди, стейкхолдеры (мужики, держащие в руках кусок жареного мяса). Поскольку массовые взломы не приводят к уменьшению размеров куска мяса в их руках, и вообще они давным-давно научились рисовать себе деньги из воздуха, в компаниях ничего меняться не будет.

Они? (я так и знал, это заговор любителей шашлыков)

<=============================================================================================================================================================================================================>

Здравствуйте, Pzz, Вы писали:

C>>Так вроде примеры неплохо гуглятся Idris-подобные языки позволяют описывать зависимые типы (завтипы по-русски) и проверять их целостность на этапе компиляции. Завтипы это типы данных, зависящие от данных Например, не просто "строка", а "строка-палиндром".

Pzz>А не получится ли так, что мы вместо одной программы будем писать две, сравнимого размера? Одна будет в рантайме чего-то делать, другая будет во время компиляции проверять, что первая деляет всё правильно.

Ага, ага. Вы это уже делаете — в виде тестов. Если они у вас конечно есть. И ещё ручного тестирования, если вы конечно его проводите.

А в случае известного мне вида доказуемого кода, тесты — это декларации о том, что должен делать код, а сверкой деклараций и самого кода занимается верификатор, SMT.

Здравствуйте, m2user, Вы писали:

Image: DaaN50DBSCiWPPQK7MpwIQ.webp


M>Они? (я так и знал, это заговор любителей шашлыков)
M>
M>
M>

M>
M>
M>

<=============================================================================================================================================================================================================>

Да, именно. Вот эти, бумера мордатенькие.
Для описания вот этого человеческого типажа существует более выразительная картинка, из старой игры Carmageddon, владелец трактора (фермер) Don Dumpster:



По ссылке ещё много https://carmageddon.fandom.com/wiki/Don_Dumpster

С>А в случае известного мне вида доказуемого кода, тесты — это декларации о том, что должен делать код, а сверкой деклараций и самого кода занимается верификатор, SMT.

вид известен, а код — нет, т.к. написать его ни у кого сил не хватает
в отличие от презренных тестов и т.п.

Здравствуйте, koenig, Вы писали:

С>>А в случае известного мне вида доказуемого кода, тесты — это декларации о том, что должен делать код, а сверкой деклараций и самого кода занимается верификатор, SMT.

K>вид известен, а код — нет, т.к. написать его ни у кого сил не хватает
K>в отличие от презренных тестов и т.п.

Примерно в каждом смартфоне имеется радиомодуль и ещё несколько связанных частей, там как раз такой код и находится, и туда пока что ни один хакер не залез. Я сейчас не вспомню точное название проекта, это малоизвестная штука, европейская.

Здравствуйте, Pzz, Вы писали:

Pzz>А не получится ли так, что мы вместо одной программы будем писать две, сравнимого размера? Одна будет в рантайме чего-то делать, другая будет во время компиляции проверять, что первая деляет всё правильно.

С точки зрения написания кода — нет. С точки зрения того, что происходит во время компиляции — да. Один из багов Idris это как раз случай, когда компиляция занимает бесконечное время Но если без шуток, то завтипы тем и хороши, что, подобно дженерикам, происходит своего рода type erasure во время компиляции, и код получается вполне компактным.

С>Примерно в каждом смартфоне имеется радиомодуль и ещё несколько связанных частей, там как раз такой код и находится, и туда пока что ни один хакер не залез. Я сейчас не вспомню точное название проекта, это малоизвестная штука, европейская.

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

Здравствуйте, Артём, Вы писали:

Аё>Например, в типизированных/типобезопастых языках, проверка типов не гарантирует отсутствие багов. Но, в сравнении с динамическими, по крайней мере там компилятор помогает отлавливать глупые ошибки- когда в одном месте поменял, а в другом забыл.
Аё>Чем помогает "доказуемый код"?
Тем же самым. "Тип" в типизированном/типобезопасном языке и есть некоторый контракт. Правда, в мейнстримных языках этот контракт а) весьма урезан и б) его надо выводить руками.
Собственно, "зависимые типы" — это и есть попытка усложнить спецификацию типа так, чтобы она позволяла описывать более интересные контракты.
Потому что альтернатива — это Дийкстра/Хоар, где к каждой функции помимо типов аргументов и возвращаемого результата надо ещё писать предусловия и постусловия (а к каждому циклу — инвариант).

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

Здравствуйте, Sinclair, Вы писали:

S>Потому что альтернатива — это Дийкстра/Хоар, где к каждой функции помимо типов аргументов и возвращаемого результата надо ещё писать предусловия и постусловия (а к каждому циклу — инвариант).

Ну нет, есть ещё трансляция кода в CoQ с последующими доказательствами, например. Другое дело, что и Idris, и CoQ сейчас находятся на уровне "вот ещё одна публикация", а пре- и пост-условия это реальность, давно используемая в SPARK. Или же я не знаю про промышленные проекты на Idris, Agda, CoQ

Здравствуйте, Sinclair, Вы писали:


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

В typescript можно указать "только эти значения возможны", но нет "неотрицательное". А как в общем 3омпилятор мож5т знать "неотрицательное" кроме 4ак рантаймом? Что замедлит исполнение.

Здравствуйте, cppguard, Вы писали:
C>Ну нет, есть ещё трансляция кода в CoQ с последующими доказательствами, например.
А что, CoQ каким-то волшебным образом угадает намерения программиста, и сможет доказывать корректность неаннотированных программ?

Здравствуйте, Артём, Вы писали:

Аё>В typescript можно указать "только эти значения возможны", но нет "неотрицательное". А как в общем 3омпилятор мож5т знать "неотрицательное" кроме 4ак рантаймом? Что замедлит исполнение.
Прекрасно он может знать. У нас в половине промышленных ЯП есть поддержка беззнаковых целых.
Если хочется строгости, то достаточно убрать неявные конверсии между знаковыми и беззнаковыми, плюс продвинутый вывод типов, и всё получится.
Да, на границах взаимодействия придётся втыкать рантайм проверки (впрочем, в реальном коде их и так делают — если хотят, чтобы он всё-таки работал), но "внутри" компилятор избыточные проверки может устранить.
Например, если мы умножаем signed byte сам на себя, то результат гарантированно влезет в unsigned short без каких-либо проверок.