5 ms·

Not every optionally typed system is gradually typed. The purpose of gradual typing is to allow typed and untyped code to interact (0) without destroying the s

Not every optionally typed system is gradually typed. The purpose of gradual typing is to allow typed and untyped code to interact (0) without destroying the safety guarantees of typed code, (1) correctly assigning blame, if a runtime type error happens, to the specific untyped part of the program that causes the error. Common Lisp's optional types don't quite fit the bill.

fiddlerwoaroof 9y ago
(check-type foo string) Does: it asserts the type of the place and throws a (restartable) error, giving the user a chance to fix the problematic value rather than bailing. I guess they don't really solve (1), but the stack trace that arises is a start.
- catnaroek 9y ago
  Stack traces contain a lot of information. Most of it is useless garbage. Yet at the same time sometimes stack traces don't contain the information you need. Making them even more useless garbage.
  - tehwalrus 9y ago
    Hogwash. Stack traces in multi-threaded applications are much much more useful than just an exception name, or even just the site of the exception.
    - catnaroek 9y ago
      What I need is the proof that the program is correct. Bugs will show up as gaps or inconsistencies in the proof. But, in the absence of even an attempt at a proof, all I can do is throw the program to the dogs.
      - tehwalrus 9y ago
        I've never yet had the luxury of working in a language that admitted formal proofs of correctness. Do you mean informal "proofs" like unit tests? When a bug occurs (perhaps because your tests did not anticipate every edge case) how do you determine where the problem code is located without a stack trace? I know that it doesn't usually point to the line of code that is problematic, but it usually gives you a starting point for your deductions...
        catnaroek 9y ago
        > I've never yet had the luxury of working in a language that admitted formal proofs of correctness. You don't need much from your language, except for a formal semantics. But, even if your language of choice doesn't have one, you can stick to a subset of it that is easy to formalize: no first-class procedures (or things that can simulate them, such as dynamic method dispatch), no non-local control flow operators (e.g. raising and handling exceptions), no non-lexical variables, just statically dispatched procedures and structured control flow constructs (selection and repetition, i.e., pattern matching and recursion). > When a bug occurs (perhaps because your tests did not anticipate every edge case) how do you determine where the problem code is located without a stack trace? By reasoning about every statement's intended and actual preconditions and postconditions, i.e., predicates on the program's free variables. At some point, the intended and actual preconditions of a statement-postcondition pair won't agree. But this is unreasonably hard if you need to reconstruct these preconditions and postconditions completely from scratch.
        tehwalrus 9y ago
        I've never had the luxury of that much control over a codebase in the real world of work.
      - TheCoelacanth 9y ago
        It seems pretty useless to even try to formally verify a program when all of the dependencies that are necessary to do anything useful are not formally verified. Where do I find a formally verified TCP/IP stack, a formally verified database, a formally verified HTML/CSS renderer, etc.?

fiddlerwoaroof 9y ago

(check-type foo string) Does: it asserts the type of the place and throws a (restartable) error, giving the user a chance to fix the problematic value rather than bailing. I guess they don't really solve (1), but the stack trace that arises is a start.

catnaroek 9y ago
Stack traces contain a lot of information. Most of it is useless garbage. Yet at the same time sometimes stack traces don't contain the information you need. Making them even more useless garbage.
- tehwalrus 9y ago
  Hogwash. Stack traces in multi-threaded applications are much much more useful than just an exception name, or even just the site of the exception.
  - catnaroek 9y ago
    What I need is the proof that the program is correct. Bugs will show up as gaps or inconsistencies in the proof. But, in the absence of even an attempt at a proof, all I can do is throw the program to the dogs.
    - tehwalrus 9y ago
      I've never yet had the luxury of working in a language that admitted formal proofs of correctness. Do you mean informal "proofs" like unit tests? When a bug occurs (perhaps because your tests did not anticipate every edge case) how do you determine where the problem code is located without a stack trace? I know that it doesn't usually point to the line of code that is problematic, but it usually gives you a starting point for your deductions...
      - catnaroek 9y ago
        > I've never yet had the luxury of working in a language that admitted formal proofs of correctness. You don't need much from your language, except for a formal semantics. But, even if your language of choice doesn't have one, you can stick to a subset of it that is easy to formalize: no first-class procedures (or things that can simulate them, such as dynamic method dispatch), no non-local control flow operators (e.g. raising and handling exceptions), no non-lexical variables, just statically dispatched procedures and structured control flow constructs (selection and repetition, i.e., pattern matching and recursion). > When a bug occurs (perhaps because your tests did not anticipate every edge case) how do you determine where the problem code is located without a stack trace? By reasoning about every statement's intended and actual preconditions and postconditions, i.e., predicates on the program's free variables. At some point, the intended and actual preconditions of a statement-postcondition pair won't agree. But this is unreasonably hard if you need to reconstruct these preconditions and postconditions completely from scratch.
        tehwalrus 9y ago
        I've never had the luxury of that much control over a codebase in the real world of work.
    - TheCoelacanth 9y ago
      It seems pretty useless to even try to formally verify a program when all of the dependencies that are necessary to do anything useful are not formally verified. Where do I find a formally verified TCP/IP stack, a formally verified database, a formally verified HTML/CSS renderer, etc.?