3 ms·
It’s been very difficult for me to devote any time to dependent type theory and it’s associated programming languages. It seems incredibly complicated for fairl
by amw-zero 6y ago
It’s been very difficult for me to devote any time to dependent type theory and it’s associated programming languages. It seems incredibly complicated for fairly little gain, since mis-specifying programs is so common.
I’m much more fond of the TLA+ style thinking of using simple untyped set theory and model-checking to verify computations.