Comment by IshKebab
8 hours ago
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?
8 hours ago
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?
https://xenaproject.wordpress.com/2020/07/05/division-by-zer...
> But it doesn’t lead to confusion when doing mathematics in a theorem prover.
This is demonstrably untrue.
In any case that post is pretty unpersuasive. Basically saying it's too tedious to do it right, in a language whose whole purpose is tediously doing things right!
Probably the better conclusion is that more proof automation is needed for simple things like "this number is not negative" so it is less tedious.
(I'm not a Lean expert but I was totally put off by it happily accept a uint8 with value 300.)