foreverglade (@foreverglade)

In F* you can write an increment function whose result is always one more than the input you give in. Additionally, F* will prove that this function is total which includes proving that it always terminates in a finite amount of time. val incr : a : UInt64.t{UInt64.v a < max_int UInt64.n} -> b : UInt64.t{lt a b} let incr x = x +^ 1uL This can be compiled with KreMLin into uint64_t Hello_incr(uint64_t x) { return x + (uint64_t)1U; }