Who said anything about “limiting”? I find it helps me understand things. Using types doesn’t rule out using other methods.
-
-
Replying to @edwinbrady @pressron
Sometimes I also find it useful to state properties as types but leave them as axioms. It’s up to the programmer to decide when to stop.
1 reply 0 retweets 3 likes -
Replying to @edwinbrady
Proofs and axioms are far from the only ways to use propositions. In fact, when it comes to programs (rather than math), I would say that they are the two worst ways. One promises everything yet provides little, and the other is too costly and provides too much (usually).
2 replies 0 retweets 3 likes -
Replying to @pressron @edwinbrady
What would you say are the top best ways?
1 reply 0 retweets 0 likes -
Replying to @PLT_cheater @edwinbrady
Fully automated, though weaker ways: static analysis/automated proof of weakened properties, model checking (possibly of finite instance), concolic tests (generated from spec), randomized tests (generated from spec), assertions (generated from spec).
1 reply 0 retweets 1 like -
By weakened properties for I mean a spec that says that the output must be prime, and the tool says, well, I can’t automatically prove primality, but I can automatically prove the number is odd. You can then automatically generate tests/assertions for primality.
1 reply 0 retweets 1 like -
-
Replying to @PLT_cheater @edwinbrady
The first rule of software specification is that the precision of the spec should not be related to the means/strength of verification. The spec should be precise, but you can choose to prove a weaker property and/or use weaker verification.
1 reply 0 retweets 1 like -
Replying to @pressron @PLT_cheater
The whole point of my thread was that dependent types are about much more than specification, and discussions always assume otherwise.
1 reply 0 retweets 0 likes -
Replying to @edwinbrady @PLT_cheater
Alright, but that’s what I’m having a hard time understanding. What’s the difference between “expressing your understanding” and writing an invariant? And your linking of “specification and proof” confused me further because in formal methods we (try to) separate the two.
1 reply 0 retweets 0 likes
Fair enough. I can see we’re never going to agree here, so I’m going to do productive things. I hope all our favoured methods work out!
-
-
Replying to @edwinbrady @PLT_cheater
NP, although if you feel like it, I really would like to know what you meant by “an understanding” which is different from a formal invariant. It’s just that in the terminology I’m used to, what you wrote sounded like “DTs aren’t about X — they’re about X”.
1 reply 0 retweets 0 likes -
This Tweet is unavailable.
New conversation -
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.