3 ms·
> Microsoft Z3 recently (a kind of theorem prover) Also a theorem prover with kinds (or more one type of elements), if I'm not mistaken :-) Firefox is getting
by bjarneh 6y ago
> Microsoft Z3 recently (a kind of theorem prover)
Also a theorem prover with kinds (or more one type of elements), if I'm not mistaken :-)
Firefox is getting really good; perhaps a bit memory hungry, but that's hardly where Chrome shines either...
- jlokier 6y agoThey call them sorts not kinds :-) "Sort" comes from many-sorted logic where the sort distinction is at the syntactic level, so easily inferred. They are not called "types" because they don't come from type theory; there is no logical richness to the relationships between different sorts, unlike the relationships between types. They are not called "kinds" because that is the name of a higher-order concept in type theory.