Ah ok, not sure how I missed that. That still seems to be within the realm of a ... | Hacker News

Hacker Newsnew | past | comments | ask | show | jobs | submit

		lwb on Feb 5, 2020 \| parent \| context \| favorite \| on: ZZ is a modern formally provable dialect of C 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?

augusto-moura on Feb 5, 2020 | [–]

Well 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

[2] https://en.wikipedia.org/wiki/Type_theory

[3] https://en.wikipedia.org/wiki/Foundations_of_mathematics

ludamad on Feb 5, 2020 | [–]

Dependent type systems certainly are!

Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact