4 ms·
Ah ok, not sure how I missed that. That still seems to be within the realm of a type system, no? Or would you consider type systems a subset of mathematically p
by lwb 7y ago
Ah ok, not sure how I missed that. That still seems to be within the realm of a type system, no? Or would you consider type systems a subset of mathematically provable systems?
- ludamad 7y agoDependent type systems certainly are!
- augusto-moura 7y agoWell Type Theory is actually one of the definitions of mathematics and computation[1]. Wikipedia gives a basic definition of it [2][3] [1] https://en.wikipedia.org/wiki/Typed_lambda_calculus https://en.wikipedia.org/wiki/Typed_lambda_calculus [2] https://en.wikipedia.org/wiki/Type_theory https://en.wikipedia.org/wiki/Type_theory [3] https://en.wikipedia.org/wiki/Foundations_of_mathematics https://en.wikipedia.org/wiki/Foundations_of_mathematics