2 ms·
I'd prefer stronger methods like logic proofs and constraint or contract specifications. Compilers could use those even better to optimize and check the meaning
by AstralStorm 8y ago
I'd prefer stronger methods like logic proofs and constraint or contract specifications. Compilers could use those even better to optimize and check the meaning of the program.
Types are very limited logic constraints after all.
While at it, you could ditch some of the old language.
Ultimately, everything is just some place in memory, cache and/or CPU register.
- icebraining 8y agoDependent types can encode constraints and require proofs.
- AstralStorm 8y agoYes they do. In a supremely roundabout way typically making for ugly fat proofs for anything high order. Sometimes, rarely, they make proofs cleaner and more direct than high order logic. Plus there is the potential undecidability if you want to use automated type deduction. Hard to spot where the types have to be so to speak reified with bad error messages.