- Не всё может быть проверено в compile-time, боюсь. То есть в коде, который может быть представлен в виде конечного автомата и который вполне верифицируется, оно таки да. Но не в общем случае - а ну как генетический или иммунный или нейроалгоритм с рандомизатором? Правда я человек темный, может быть уже есть крутой math и на такой случай.
В Аде в compile-time может быть проверен выход за пределы диапазона, но только если значение выводимо именно на момент компиляции, а это мягко говоря не всегда так.
- Тут два момента - во-первых в приложениях, где требуется надежность просто подход - те методы, про которые нельзя просто и понятно (в том числе компилятору) объяснить что все работает - и не стоит использовать.
Во-вторых - один из самых простых методов такого объяснения - это именно явная проверка:
module My2 type byte = i:nat{0 <= i && i < 255 } let read_int = FStar.IO.input_int val read_byte : unit -> byte let read_byte () = read_int ()
При компиляции ругается:
/my2.fst(8,19-8,30): Subtyping check failed; expected type byte; got type int
А если переписать:
exception InvalidByte val read_byte : unit -> byte let read_byte () = let i = read_int () in if 0 <= i && i < 256 then i else raise InvalidByte
То все ок - точнее в том коде который тут наверху - тоже ругается - потому что там ошибка - верхняя граница байта неверно указана - но если поправить 255 на 256 как и надо - все ОК.
Но проверку самому надо написать - компилятор за тебя ее не сделает
PS: И дело не в том, что константы (и даже не в том, что арифметика - там в принципе можно и с любыми в принципе типами такие вещи писать):
exception InvalidRange val read_range : l:int -> u:int -> i:int{l <= i && i <= u} let read_range l u = let i = read_int () in if l <= i && i <= u then i else raise InvalidRange val a : byte let a = read_range 0 255
Тоже работает - и вовсе не потому что компилятор "инлайнит" - а именно потому что из типа read_range вытекает что его применение к 0 255 даст именно byte.
То есть с раздельной компиляцией это все точно так же работает
Ситуации, когда интеллекта компилятора действительно не хватит естественно тоже есть - но и там обычно можно компилятору "подсказать" "почему это правда" (то есть дать доказательство/схему доказательства, до которых он сам допереть не может)