3 ms·
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 u
by IshKebab 3mo 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?
- gugagore 3mo agohttps://xenaproject.wordpress.com/2020/07/05/division-by-zero-in-type-theory-a-faq/ https://xenaproject.wordpress.com/2020/07/05/division-by-zer...
- IshKebab 3mo ago> 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.)