3 ms·
As you say, the big problem is you can’t express rules. I don’t think that rules out using code to understand these things, but you’re better off starting with
by moomin 7y ago
As you say, the big problem is you can’t express rules. I don’t think that rules out using code to understand these things, but you’re better off starting with something like LEAN.
- reikonomusha 7y agoIt’s one of the issues. The other is that you quickly will want to work with these algebraic structures as objects themselves. When the algebraic structure is encoded as a protocol, you won’t be able to manipulate them as first-class values. For instance, you’ll want this if you want to do things like factorizing groups, constructing products (like the semi direct product), computing graded algebras, computing homomorphisms, constructing Groebner bases, etc.
- moomin 7y agoYeah, you need dependent typing to do that in a programming language. But as cool as dependently typed languages are, developing serious software in them remains a bit of a research problem. Idris is closest, but it also less convenient for actual proofs.