F* seems to be a collection of like five different languages and proof systems. Honestly I never figured it out.

Does it get basic stuff like subtraction and u8 right, unlike Lean?