- Не всё может быть проверено в 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.
То есть с раздельной компиляцией это все точно так же работает
Ситуации, когда интеллекта компилятора действительно не хватит естественно тоже есть - но и там обычно можно компилятору "подсказать" "почему это правда" (то есть дать доказательство/схему доказательства, до которых он сам допереть не может)
