История изменений

Насколько я понимаю, в идрисе можно указать, что тип линейный (а можно не указывать).

Да, это верно, на сколько я помню. Спасибо за пояснение. Действительно, подход раста с этой т.з. выглядит интересно на мой взгляд (который состоит в том что лучше бы компилятор проверял всё до чего дотянется).

Кстати, флоатинг поинт вполне себе верифицируется

http://iste.co.uk/book.php?id=1238

Я книжку правда не читал, но таки подход описан и похоже можно пользоваться. Мне правда не надо, вещественные числа меня пока не задевают, а там кто знает, конечно...

Насколько я понимаю, в идрисе можно указать, что тип линейный (а можно не указывать).

Да, это верно, на сколько я помню. Спасибо за пояснение. Действительно, подход раста с этой т.з. выглядит интересно на мой взгляд (который состоит в том что лучше бы компилятор проверял всё до чего дотянется).

Кстати, флоатинг поинт вполне себе верифицируется

http://iste.co.uk/book.php?id=1238