Можно. И даже в vscode писать из под Windows.

мне по идее за глаза хватит. Надо ли этот Ризон (хипстерский?) %)

а блин, я же автоматические тесты хотела добавить

а блин, я же автоматические тесты хотела добавить

А какие проблемы?

А какие проблемы?

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

Понял.

всякие джавы-сиплюсплюсы изкаропки там

Понял.

А ты из универа свалил? Вроде писал нечто подобное

моя мечта - заставить студентов самих друг у друга лабы проверять, но это ещё сложнее автоматически сделать :) Надо как peer review в курсере

А ты из универа свалил? Вроде писал нечто подобное

Я в аспирантуре, но не преподаю больше.

Понятно

кстати, вы знаете про F*? https://en.wikipedia.org/wiki/F*_(programming_language)

А он во что компилируется?

А он во что компилируется?

Он не для компиляции в исполняемые файлы.

Он не для компиляции в исполняемые файлы.

А для чего?

А он во что компилируется?

он верифицирует. Типы переводятся в C

Можно экстрактить код в OCaml или C.

Можно экстрактить код в OCaml или C.

о, а как?

F* пока выглядит для меня как матан высшего порядка :(

Хотя для общего образования полезно, наверное

о, а как?

Я не знаю, посмотри флаги компилятора. :)

Я так понимаю, он руки отрезает значительно жёстче, чем f#

Намертво, не пришить.

Но в нём конечно тайп инфиренс ядерный из этого кода let rec factorial n = if n = 0 then 1 else n * (factorial (n - 1)) оно выводит такой тип: val factorial: x:int{x>=0} -> Tot int т.е. поняло что >=0 и что на выходе Tot int, тотальная функция

Кстати, неясно,как вывели

Можно экстрактить код в OCaml или C.

То есть ты на F* верифицируешь, а потом генеришь соответствующий код, который потом работает?

Что >=0

Что >=0

ну по коду ясно же

Неясно

ну по коду ясно же

вроде же можно отрицательный x передать, ичо

вроде же можно отрицательный x передать, ичо

Вот и я о том

при нуле - ноль, меньше нуля - уход в бесконеность - больше все сходится к инту

стоп, я прогнал

при нуле - ноль, меньше нуля - уход в бесконеность - больше все сходится к инту

а бесконечность приведет к стековерфлоу

именно

Ну дык -2 можно подсунуть

Там ещё is_positive

В теории 😉

оно не так работает For a recursive function, without further annotation, F* attempts to automatically prove that the recursion always terminates. In the case of factorial above, F* attempts to prove that it has type int -> Tot int, and fails to do so because, factorial is actually not a total function on arbitrary integers! Think about factorial -1.

x>=0 это может оно и есть? Условия, при которых работает и тотальное?

The factorial function is, however, a total function on non-negative integers. We can ask F* to check that this is indeed the case by writing: val factorial: x:int{x>=0} -> Tot int

Once we write this down, F* automatically proves that factorial satisfies all these properties.

The factorial function is, however, a total function on non-negative integers. We can ask F* to check that this is indeed the case by writing: val factorial: x:int{x>=0} -> Tot int

а, ты ему сам говоришь условия, а он проверяет

да. Но т.к. есть тайп инфиринс, то функция примет такой тип

Там вначале пишется сигнатура с условиями

т.е. ты аннотируешь условие и это условие идёт в тип функции

Ну ладно, кажется я немного поумнела

Вот прямо в спеке ихней

В общем, такой способ метаданные вкрутить

Как я понимаю

ну. Почти) Там в типе может быть отображено что функция расходится например или аллоцирует!

Ну метаданные же

Ну если ты типы называешь метаданными, то пусть будут метаданными)))

Так.Стоп

Мы сначала описываем тип функции, потом его имплементируем?

это называется refinment type типа

ype f:filename{canRead f} is a refinement of the type filename

т.е. можно быстро создавать подмножества типов, которые тоже типы очевидно (потому что тоже множества)

Штука интересная, но чтобы применить в продакшне, надо быть очень умным

Кмк

Так точно, оно неприменимо для 99.99999% задач

но вообще верифицирующие языки применяются. Их не один

Ну из очевидных применений ,очевидно ,криптография

Там как раз верификация алгоритма важна

Хозяйственный мужчина никому не нужен?

Так точно, оно неприменимо для 99.99999% задач

Было бы интересно поработать над этой 0.00001%.

Именно в индустрии, а не академии. :)

Fucken nerds... 💔

> () {} ;

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

Для финтеха выглядит интересно

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

Получается довольно низкоуровневая вещь

> () {} ;

()[]{}();

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

Базы данных, распределенные системы.

Базы данных, распределенные системы.

Да, похоже на то

Файловые системы, кстати

Ещё, возможно, протоколы обмена данными

Но тут очень спорный момент

В общем всё, где есть пользовательские данные, идёт мимо