On: Verified Programming in F*: A Tutorial

[amw-zero]

Try reading the tutorial. F* uses refinement types, which means that logic is checked before the program is executed, at compile time.