3 ms·

> Side note: I expected to see mention of design by contract and function preconditions/invariants/postconditions. For some reason, DbC seems to be virtually u

> Side note: I expected to see mention of design by contract and function preconditions/invariants/postconditions. For some reason, DbC seems to be virtually unknown to most programmers. It's incredibly strange: I was sure that DbC would be the next big step after gradual typing. It's just such a natural fit: where the type system gives up (any/dynamic), the contract system can step in. There are papers on automatically generating contracts from types (and vice versa) to allow typed values to flow through untyped code; there are papers showing how to make that performant enough; papers showing how to instrument systems to generate types and contracts from tests; etc. They are all 15-20 years old now, yet there's still nothing suggesting that the mainstream even looks that way, much less actually implements something usable.

rramadass 2mo ago
Can you share the links to all the papers that you refer to?
- klibertp 2mo ago
  The ones I most likely had in mind (recovered with help from ChatGPT due to my memory being fuzzy - but most links it produced were in my bookmarks): - Matthias Felleisen, Sam Tobin-Hochstadt, “Interlanguage Migration: From Scripts to Programs” (DLS 2006) - Sam Tobin-Hochstadt, Matthias Felleisen, “The Design and Implementation of Typed Scheme” (POPL 2008) - Sam Tobin-Hochstadt, “Typed Scheme: From Scripts to Programs” (2010). - Asumu Takikawa et al., “Gradual Typing for First-Class Classes” (OOPSLA 2012) - Esteban Allende, Johan Fabry, Éric Tanter, “Cast Insertion Strategies for Gradually-Typed Objects” (DLS 2013) - Esteban Allende, Johan Fabry, Ronald Garcia, Éric Tanter, “Confined Gradual Typing” (OOPSLA 2014). - Nadia Polikarpova, Ilinca Ciupa, Bertrand Meyer, “A Comparative Study of Programmer-Written and Automatically Inferred Contracts” (ISSTA 2009). There's a lot more research and literature on the topic. Naive approaches were tried ~2010 and were shown to be performance disasters, but by ~2015 we already had those issues mostly solved. I seriously thought that every new language (or new release of an existing PL) after that would feature first-class support for contracts and gradual typing, along with built-in support for automatically generating/harvesting types and contracts from tests. It's 2026, and the mainstream still doesn't seem aware of the possibilities, much less actively going in that direction. It's nuts!
  - rramadass 2mo ago
    Thank You and Appreciate it very much! The 1st, 4th and 7th papers look especially interesting. I think in order to appreciate DbC (gradual typing is whole another beast altogether) one needs to have some idea of "Program Correctness" concepts in the lineage of Floyd/Hoare/Dijkstra and Meyer. With LLMs it is even more important to use the above as a "Correctness-by-Construction" (CbC) approach to code generation. To me this is the need of the hour and yet i don't see people talking about it; Correctness-by-Construction (CbC) - https://www.tu-braunschweig.de/en/isf/research/cbc https://www.tu-braunschweig.de/en/isf/research/cbc Correctness-by-Construction: An Overview of the CorC Ecosystem by Bordis, Runge et al. - https://dl.acm.org/doi/10.1145/3591335.3591343 https://dl.acm.org/doi/10.1145/3591335.3591343 The Correctness-by-Construction Approach to Programming by Derrick Kourie and Bruce Watson - https://link.springer.com/book/10.1007/978-3-642-27919-5 https://link.springer.com/book/10.1007/978-3-642-27919-5
    - klibertp 2mo ago
      > I think in order to appreciate DbC [...] one needs to have some idea of "Program Correctness" concepts in the lineage of Floyd/Hoare/Dijkstra and Meyer. Agreed. To me, full-program (or system) formal verification is something I'd love to have, but I also acknowledge that even champions of formal methods (like Tony Hoare you mentioned) doubt its practicality, due to how large our software systems tend to be nowadays. If so, then let's take as much as we can from those methods (powerful, expressive type systems) and let's complement that with proper infrastructure for ensuring correctness (contracts, invariants, various kinds of automated tests) that are weaker, but much more applicable in practice. Unfortunately, we're still stuck in a place where a plain `assert` - basically a "goto of ensuring correctness" - needs to be introduced to people with posts like the OP's... > To me this is the need of the hour and yet i don't see people talking about it Yes, I feel the same. I think the reason here is that we (programmers, collectively) didn't really take correctness of our programs seriously before, so there's just not much awareness about the research and work done in this problem space. Many people now are ready to admit that yes, we do need stronger, more comprehensive and better integrated tools for controlling, showing, and ensuring correctness - but the need for them arrived so quickly (and along with so many other, serious changes to the craft), that they simply haven't been able to catch up on the prior work fast enough. It'll probably take a few years, at least, for the urgent need for better tools to become widely recognized. It'll take even more time to get to usable implementations. > (gradual typing is whole another beast altogether) It's actually not. Contracts in Racket are duals of types (well, not fully, since you can put arbitrary code in a predicate and make that into a contract; however, that's more of an escape hatch than the default use of contracts in Racket). Typed Racket can wrap a typed value in a contract that guarantees that, when the value comes back, it exactly conforms to its type. This way, you can avoid expensive casts. Moreover, Typed Racket has refinement types (ie. that a given int will always be greater than 0), and these refinements have direct contract equivalents, too. So a Typed Racket value can be statically proven to have that property on the typed side, and then you don't have to check or prove it again when it comes back from the untyped world. I believe this is an extremely neat capability that ties types and contracts together, opening some very interesting possibilities. Like, if a contract can be expressed as a refinement on a type, and we already have support for that in the type checker, we can automatically promote such contracts into types! That's huge, because if the contracted value never leaves a well-typed environment, we can eliminate all runtime checks without affecting correctness. It also addresses the most common problem with contracts (and assertions): runtime overhead. I'm aware of all that because I decided to build an environment that would blend a fast, interactive development loop, an isolated environment in which agents can comfortably live, and an expansive toolkit for checking and ensuring correctness. I'm building it on top of Pharo Smalltalk, Glamorous Toolkit, and an extended Gradualtalk implementation that would also handle contracts. There are some problematic parts, but if I manage to achieve my goals in a Smalltalk image, I feel like it'll prove it can be achieved in literally every other environment, too :) EDIT: Forgot to mention, there's a pretty extensive list of papers on contracts and gradual typing here: https://samth.github.io/gradual-typing-bib https://samth.github.io/gradual-typing-bib EDIT: "Types to contracts" is already presented in papers I referenced before (Typed Racket ones); forgot to mention the "contracts to types" (or rather, static verification of contracts) part: "Soft Contract Verification for Higher-Order Stateful Programs" and "Soft Contract Verification" by Phuc C. Nguyen et al.

rramadass 2mo ago

Can you share the links to all the papers that you refer to?

klibertp 2mo ago
The ones I most likely had in mind (recovered with help from ChatGPT due to my memory being fuzzy - but most links it produced were in my bookmarks): - Matthias Felleisen, Sam Tobin-Hochstadt, “Interlanguage Migration: From Scripts to Programs” (DLS 2006) - Sam Tobin-Hochstadt, Matthias Felleisen, “The Design and Implementation of Typed Scheme” (POPL 2008) - Sam Tobin-Hochstadt, “Typed Scheme: From Scripts to Programs” (2010). - Asumu Takikawa et al., “Gradual Typing for First-Class Classes” (OOPSLA 2012) - Esteban Allende, Johan Fabry, Éric Tanter, “Cast Insertion Strategies for Gradually-Typed Objects” (DLS 2013) - Esteban Allende, Johan Fabry, Ronald Garcia, Éric Tanter, “Confined Gradual Typing” (OOPSLA 2014). - Nadia Polikarpova, Ilinca Ciupa, Bertrand Meyer, “A Comparative Study of Programmer-Written and Automatically Inferred Contracts” (ISSTA 2009). There's a lot more research and literature on the topic. Naive approaches were tried ~2010 and were shown to be performance disasters, but by ~2015 we already had those issues mostly solved. I seriously thought that every new language (or new release of an existing PL) after that would feature first-class support for contracts and gradual typing, along with built-in support for automatically generating/harvesting types and contracts from tests. It's 2026, and the mainstream still doesn't seem aware of the possibilities, much less actively going in that direction. It's nuts!
- rramadass 2mo ago
  Thank You and Appreciate it very much! The 1st, 4th and 7th papers look especially interesting. I think in order to appreciate DbC (gradual typing is whole another beast altogether) one needs to have some idea of "Program Correctness" concepts in the lineage of Floyd/Hoare/Dijkstra and Meyer. With LLMs it is even more important to use the above as a "Correctness-by-Construction" (CbC) approach to code generation. To me this is the need of the hour and yet i don't see people talking about it; Correctness-by-Construction (CbC) - https://www.tu-braunschweig.de/en/isf/research/cbc https://www.tu-braunschweig.de/en/isf/research/cbc Correctness-by-Construction: An Overview of the CorC Ecosystem by Bordis, Runge et al. - https://dl.acm.org/doi/10.1145/3591335.3591343 https://dl.acm.org/doi/10.1145/3591335.3591343 The Correctness-by-Construction Approach to Programming by Derrick Kourie and Bruce Watson - https://link.springer.com/book/10.1007/978-3-642-27919-5 https://link.springer.com/book/10.1007/978-3-642-27919-5
  - klibertp 2mo ago
    > I think in order to appreciate DbC [...] one needs to have some idea of "Program Correctness" concepts in the lineage of Floyd/Hoare/Dijkstra and Meyer. Agreed. To me, full-program (or system) formal verification is something I'd love to have, but I also acknowledge that even champions of formal methods (like Tony Hoare you mentioned) doubt its practicality, due to how large our software systems tend to be nowadays. If so, then let's take as much as we can from those methods (powerful, expressive type systems) and let's complement that with proper infrastructure for ensuring correctness (contracts, invariants, various kinds of automated tests) that are weaker, but much more applicable in practice. Unfortunately, we're still stuck in a place where a plain `assert` - basically a "goto of ensuring correctness" - needs to be introduced to people with posts like the OP's... > To me this is the need of the hour and yet i don't see people talking about it Yes, I feel the same. I think the reason here is that we (programmers, collectively) didn't really take correctness of our programs seriously before, so there's just not much awareness about the research and work done in this problem space. Many people now are ready to admit that yes, we do need stronger, more comprehensive and better integrated tools for controlling, showing, and ensuring correctness - but the need for them arrived so quickly (and along with so many other, serious changes to the craft), that they simply haven't been able to catch up on the prior work fast enough. It'll probably take a few years, at least, for the urgent need for better tools to become widely recognized. It'll take even more time to get to usable implementations. > (gradual typing is whole another beast altogether) It's actually not. Contracts in Racket are duals of types (well, not fully, since you can put arbitrary code in a predicate and make that into a contract; however, that's more of an escape hatch than the default use of contracts in Racket). Typed Racket can wrap a typed value in a contract that guarantees that, when the value comes back, it exactly conforms to its type. This way, you can avoid expensive casts. Moreover, Typed Racket has refinement types (ie. that a given int will always be greater than 0), and these refinements have direct contract equivalents, too. So a Typed Racket value can be statically proven to have that property on the typed side, and then you don't have to check or prove it again when it comes back from the untyped world. I believe this is an extremely neat capability that ties types and contracts together, opening some very interesting possibilities. Like, if a contract can be expressed as a refinement on a type, and we already have support for that in the type checker, we can automatically promote such contracts into types! That's huge, because if the contracted value never leaves a well-typed environment, we can eliminate all runtime checks without affecting correctness. It also addresses the most common problem with contracts (and assertions): runtime overhead. I'm aware of all that because I decided to build an environment that would blend a fast, interactive development loop, an isolated environment in which agents can comfortably live, and an expansive toolkit for checking and ensuring correctness. I'm building it on top of Pharo Smalltalk, Glamorous Toolkit, and an extended Gradualtalk implementation that would also handle contracts. There are some problematic parts, but if I manage to achieve my goals in a Smalltalk image, I feel like it'll prove it can be achieved in literally every other environment, too :) EDIT: Forgot to mention, there's a pretty extensive list of papers on contracts and gradual typing here: https://samth.github.io/gradual-typing-bib https://samth.github.io/gradual-typing-bib EDIT: "Types to contracts" is already presented in papers I referenced before (Typed Racket ones); forgot to mention the "contracts to types" (or rather, static verification of contracts) part: "Soft Contract Verification for Higher-Order Stateful Programs" and "Soft Contract Verification" by Phuc C. Nguyen et al.