3 ms·

Maybe, but I think that's mostly an implementation issue... Not only will automated theorem provers get better, but the point is, they don't even need to prove

by tomp 8y ago

Maybe, but I think that's mostly an implementation issue... Not only will automated theorem provers get better, but the point is, they don't even need to prove anything! A program would be just as valid if you inserted runtime checks for all contracts, or just the ones you can't prove or disprove. Compare that to type systems, different languages have different ways of dealing with issues (e.g. you can disable type errors in Haskell, Python doesn't care either way, Java is unsound, Scala supports the `any` type, TypeScript defaults to `any`, etc). So we can start by putting contracts from if statements directly into types (that still compile to equivalent code with runtime checks), we immediately gain readability, then slowly but surely we'll be able to prove more and more...

lmm 8y ago
> the point is, they don't even need to prove anything! A program would be just as valid if you inserted runtime checks for all contracts, or just the ones you can't prove or disprove. "Valid" in what sense? I want my code to refuse to compile when it's broken, not compile and then fail at runtime. I certainly don't want similar-looking checks to be usually compile time but occasionally runtime when things get complicated - that way madness lies. > Compare that to type systems, different languages have different ways of dealing with issues (e.g. you can disable type errors in Haskell, Python doesn't care either way, Java is unsound, Scala supports the `any` type, TypeScript defaults to `any`, etc). You're talking about minor differences in edge cases/escape hatches. There's much more variation between different contract systems. > So we can start by putting contracts from if statements directly into types (that still compile to equivalent code with runtime checks), we immediately gain readability, then slowly but surely we'll be able to prove more and more... Sounds like gradual typing, which I've found a nightmare to work with in practice - all the pain but very little of the gain. Being 95% typechecked (or 95% statically checked) turns out to be a lot like being 0% typechecked.
- tomp 8y ago
  > Being 95% typechecked (or 95% statically checked) turns out to be a lot like being 0% typechecked. That's just not realistic. All practical languages (even Rust and Haskell) fail for "division by zero", and most (all?) (again even Rust and Haskell) offer escape hatches for their otherwise rather strong static checks. Still (some) people see a lot of value in _more_ static (type/contract) checking.
  - lmm 8y ago
    > All practical languages (even Rust and Haskell) fail for "division by zero" Well, they don't have dependent types. In something like Idris you can do safe natural division. > most (all?) (again even Rust and Haskell) offer escape hatches for their otherwise rather strong static checks. The difference is that those escape hatches are explicit, and used rarely enough that you can give them special attention in testing/code review - in those languages it's not 95% typechecked but more like 99.9%. (Indeed in Haskell you can use a flag to disallow bypassing the typesystem entirely, and people do).
- coldtea 8y ago
  >Sounds like gradual typing, which I've found a nightmare to work with in practice - all the pain but very little of the gain. 1) How is "gradual typing" any worse than (at worst case) dynamic typing? And even more so "a nightmare"? 2) What's the big pain ("all the pain") in static strong typing? 3) How is catching 95% of type issues "very little of the gain" of catching 100% of them?
  - lmm 8y ago
    > 1) How is "gradual typing" any worse than (at worst case) dynamic typing? And even more so "a nightmare"? Type declarations that are sometimes wrong can be misleading enough that I find code with them harder to work on than code with no types at all, personally. > 2) What's the big pain ("all the pain") in static strong typing? It's not a huge pain, but adding and maintaining types does have a cost (particularly when tooling support is limited). > 3) How is catching 95% of type issues "very little of the gain" of catching 100% of them? Because you can't trust the types to be correct in any given piece of code. You end up having to do all the things you would have to do in an untyped languge (high test coverage, carefully rechecking all the types when debugging issues, etc.).
    - tomp 8y ago
      > that are sometimes wrong That's not gradual typing, just the most common implementation of gradual typing (e.g. in Dart, TypeScript, Python, but not e.g. in Clojure and Perl 6 AFAIK). Although maybe this is just a "no true Scotsman" argument...

by tomp 8y ago

lmm 8y ago

> the point is, they don't even need to prove anything! A program would be just as valid if you inserted runtime checks for all contracts, or just the ones you can't prove or disprove. "Valid" in what sense? I want my code to refuse to compile when it's broken, not compile and then fail at runtime. I certainly don't want similar-looking checks to be usually compile time but occasionally runtime when things get complicated - that way madness lies. > Compare that to type systems, different languages have different ways of dealing with issues (e.g. you can disable type errors in Haskell, Python doesn't care either way, Java is unsound, Scala supports the `any` type, TypeScript defaults to `any`, etc). You're talking about minor differences in edge cases/escape hatches. There's much more variation between different contract systems. > So we can start by putting contracts from if statements directly into types (that still compile to equivalent code with runtime checks), we immediately gain readability, then slowly but surely we'll be able to prove more and more... Sounds like gradual typing, which I've found a nightmare to work with in practice - all the pain but very little of the gain. Being 95% typechecked (or 95% statically checked) turns out to be a lot like being 0% typechecked.

tomp 8y ago
> Being 95% typechecked (or 95% statically checked) turns out to be a lot like being 0% typechecked. That's just not realistic. All practical languages (even Rust and Haskell) fail for "division by zero", and most (all?) (again even Rust and Haskell) offer escape hatches for their otherwise rather strong static checks. Still (some) people see a lot of value in _more_ static (type/contract) checking.
- lmm 8y ago
  > All practical languages (even Rust and Haskell) fail for "division by zero" Well, they don't have dependent types. In something like Idris you can do safe natural division. > most (all?) (again even Rust and Haskell) offer escape hatches for their otherwise rather strong static checks. The difference is that those escape hatches are explicit, and used rarely enough that you can give them special attention in testing/code review - in those languages it's not 95% typechecked but more like 99.9%. (Indeed in Haskell you can use a flag to disallow bypassing the typesystem entirely, and people do).
coldtea 8y ago
>Sounds like gradual typing, which I've found a nightmare to work with in practice - all the pain but very little of the gain. 1) How is "gradual typing" any worse than (at worst case) dynamic typing? And even more so "a nightmare"? 2) What's the big pain ("all the pain") in static strong typing? 3) How is catching 95% of type issues "very little of the gain" of catching 100% of them?
- lmm 8y ago
  > 1) How is "gradual typing" any worse than (at worst case) dynamic typing? And even more so "a nightmare"? Type declarations that are sometimes wrong can be misleading enough that I find code with them harder to work on than code with no types at all, personally. > 2) What's the big pain ("all the pain") in static strong typing? It's not a huge pain, but adding and maintaining types does have a cost (particularly when tooling support is limited). > 3) How is catching 95% of type issues "very little of the gain" of catching 100% of them? Because you can't trust the types to be correct in any given piece of code. You end up having to do all the things you would have to do in an untyped languge (high test coverage, carefully rechecking all the types when debugging issues, etc.).
  - tomp 8y ago
    > that are sometimes wrong That's not gradual typing, just the most common implementation of gradual typing (e.g. in Dart, TypeScript, Python, but not e.g. in Clojure and Perl 6 AFAIK). Although maybe this is just a "no true Scotsman" argument...