June 10th, 2016

Gen.Turgidson

По поводу Холмогория

Никто кстати кажется даже не вспомнил, что за 300 лет до этого в роли индусов выступили сами англичане:

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

Тут кстати чисто финансовый и торговый фактор (ну мощное производство, которому было нужно сырье) - без военного. Результат в целом схож.
Dr.Strangelove

Все на теже типовые темы и про "проверку индексов"

К http://kouzdra.livejournal.com/3027485.html?view=comments

Норот видимо не понимает о чем идет речь:

Напомню, что в Паскале при обращении к массиву индексы компилятору проверять не надо. Проверка там выполняется (если надо) при преобразовании integer к индексному типу массива l..u

То есть если ты опишешь индексную переменную сразу как l..u - то никаких run-time проверок в простых случаях (типа цикла от l до u) и не надо.

Ну так вот тип 1..10 в этих терминах и есть { i : int | i >= 1 && i <= 10 }

Диапазонный тип как раз и есть частный встроенный ad hoc в язык случай refined types.

Отличие от Паскаля только в том что неявные приведения с run-time проверкой не предполагаются. С другой стороны - средства для доказательства того что тип в действительности такой намного мощнее - включают в себя кроме прочего general purpose дедуктивную систему. И если компилятор не способен сам убедиться что "все хорошо" - есть масса способов ему это "подсказать" (вплоть до явного выписывания прямого доказательства).
Dr.Strangelove

Еще про типы - пример из комментов:

http://kouzdra.livejournal.com/3028355.html?thread=101372035#t101372035
- Не всё может быть проверено в compile-time, боюсь. То есть в коде, который может быть представлен в виде конечного автомата и который вполне верифицируется, оно таки да. Но не в общем случае - а ну как генетический или иммунный или нейроалгоритм с рандомизатором? Правда я человек темный, может быть уже есть крутой math и на такой случай.

В Аде в compile-time может быть проверен выход за пределы диапазона, но только если значение выводимо именно на момент компиляции, а это мягко говоря не всегда так.

- Тут два момента - во-первых в приложениях, где требуется надежность просто подход - те методы, про которые нельзя просто и понятно (в том числе компилятору) объяснить что все работает - и не стоит использовать.

Во-вторых - один из самых простых методов такого объяснения - это именно явная проверка:
Collapse )