3 ms·

Advanced type systems can prove more complex properties of your program; there will theoretically always be properties we can't prove (by means of type systems

Advanced type systems can prove more complex properties of your program; there will theoretically always be properties we can't prove (by means of type systems or otherwise), and practically there will be properties that are too hard to prove. Even with dependent types, "essentially any" is an overstatement. But often times you can make important and hard-to-reason-about properties of your system "simple" from the perspective of the type system. For example, I used the C type checker to help make sure I was calling functions from the correct thread. I have a talk about it I've given a couple times - slides as C files here: https://github.com/dlthomas/using-c-types-talk/tree/master/slides https://github.com/dlthomas/using-c-types-talk/tree/master/s... - with an example program where the technique turns an occasional segfault at runtime into a "you can't call this here, dummy" error at compile time.

6gvONxR4sf7o 7y ago
There will always be things we fundamentally can't prove, but those things have no place in a program you're relying on. "Essentially any" means that any you the programmer have reason to believe and code up.
- dllthomas 7y ago
  If it's the property you need, and you can't prove it, it's still the property you need - you can't simply define it away. As I said, though, you'll almost always be hitting practical limits long before theoretical ones. And as I also said, there's still quite a few useful things we can speak meaningfully about, even in a quite impoverished setting.
ameixaseca 7y ago
I considered writing "prove any property that is provable" but it is a tautology and doesn't convey the meaning I was trying to give it. "Essentially any" can be better stated indeed as it is too broad, but I can't think of a definition right now that doesn't require a few pages of text.
- dllthomas 7y ago
  Yeah, I readily acknowledge that it's a nit. I didn't mean that portion of my comment as criticism of what you wrote, so much as rhetorical framing for my next point.

6gvONxR4sf7o 7y ago

There will always be things we fundamentally can't prove, but those things have no place in a program you're relying on. "Essentially any" means that any you the programmer have reason to believe and code up.

dllthomas 7y ago
If it's the property you need, and you can't prove it, it's still the property you need - you can't simply define it away. As I said, though, you'll almost always be hitting practical limits long before theoretical ones. And as I also said, there's still quite a few useful things we can speak meaningfully about, even in a quite impoverished setting.

ameixaseca 7y ago

I considered writing "prove any property that is provable" but it is a tautology and doesn't convey the meaning I was trying to give it. "Essentially any" can be better stated indeed as it is too broad, but I can't think of a definition right now that doesn't require a few pages of text.

dllthomas 7y ago
Yeah, I readily acknowledge that it's a nit. I didn't mean that portion of my comment as criticism of what you wrote, so much as rhetorical framing for my next point.