3 ms·

Contracts, if done right, could be used by the compiler or some dedicated linter or tester before execution. This could open up safety guarantees that are way b

Contracts, if done right, could be used by the compiler or some dedicated linter or tester before execution. This could open up safety guarantees that are way beyond what we can currently use. The question, of course, is what kind of constraint language is both useful and solvable. Unfortunately, people have been focused on the "dynamic" typing (i.e., no type checks) side of things for so long that static checking lags behind in usability (Rust is on a good way to improve things, though). Regarding first-class grammars you have to understand that it basically prohibits any other tool to parse your language. This means everyone has to fully implement the language to create any kind of small helper tool. In turn, your language might easily fall into the "exotic" camp (like, e.g., TeX - this language effectively has first-class grammars, albeit at a low level).

deleted 4y ago
[deleted]
jillesvangurp 4y ago
Kotlin has some functionality for this that help the compiler. A good example is the isNullOrBlank() extension function on String? (nullable String). It has a contract that treats the string as not null after it returns false. So if you do a null check, it smart casts to a non nullable string without generating a compile error. There are a few more variations of that in the Kotlin standard library and you can write your own contracts as well. There's just not a whole lot you can do with it other than stuff like this. But it's useful.
mejutoco 4y ago
Types in Idris sound like the contracts you mention. I learnt about them in the book "Type-Driven Development with Idris".
- mcguire 4y ago
  There is a fairly close relationship between a dependently typed language, like Idris, and 'contracts' (really, pre- and post-conditions plus other propositions) in languages like Ada/SPARK, Dafny, and Frama-C. The major differences are that most (all?) dependently typed languages are functional and require the programmer to prove the correctness of the contract in (an extension of) the language itself, while the others typically use special annotations in normal Ada/C/a generic ALGOLish language and dump the proof onto external tools like SMT solvers, all resulting in a more 'normal' programming experience.
  - throwaway17_17 4y ago
    I think liquid types, ala Liquid Haskell are a preferable middle ground in this scenario. The SMT is built into the type checker and the refinements are limited to a linearly decidable proof fragment. Dominic Orchard has done some work generalizing the capabilities of these types of refinement by showing that the refinement fragment need to just be a semi-ring structure and the SMT can still resolve. This would cover a large portion of contracts and not impart the development process in large part.
  - xmgplays 4y ago
    There is ATS as an example of an imperative language with dependent types.
6gvONxR4sf7o 4y ago
> Unfortunately, people have been focused on the "dynamic" typing (i.e., no type checks) side of things for so long that static checking lags behind in usability The longer I see things like mypy and typescript evolve, I’m actually really glad that people have been focused on gradually typing dynamic languages. As far as I can tell, really useful contracts (or really flexible types) are super burdensome in the most general cases (e.g. `refl` brain twisters in dependent types), but still insanely useful in frequent cases. It reminds me of what people say about static typing’s benefits and burdens. So I’m hoping to see the gradual typing equivalent for contracts and verification. Start with usefulness and add a spectrum of optional safety that the programmer can ignore or use as they see fit. Personally, at least, that would be my ideal scenario.

deleted 4y ago

[deleted]

jillesvangurp 4y ago

Kotlin has some functionality for this that help the compiler. A good example is the isNullOrBlank() extension function on String? (nullable String). It has a contract that treats the string as not null after it returns false. So if you do a null check, it smart casts to a non nullable string without generating a compile error. There are a few more variations of that in the Kotlin standard library and you can write your own contracts as well. There's just not a whole lot you can do with it other than stuff like this. But it's useful.

mejutoco 4y ago

Types in Idris sound like the contracts you mention. I learnt about them in the book "Type-Driven Development with Idris".

mcguire 4y ago
There is a fairly close relationship between a dependently typed language, like Idris, and 'contracts' (really, pre- and post-conditions plus other propositions) in languages like Ada/SPARK, Dafny, and Frama-C. The major differences are that most (all?) dependently typed languages are functional and require the programmer to prove the correctness of the contract in (an extension of) the language itself, while the others typically use special annotations in normal Ada/C/a generic ALGOLish language and dump the proof onto external tools like SMT solvers, all resulting in a more 'normal' programming experience.
- throwaway17_17 4y ago
  I think liquid types, ala Liquid Haskell are a preferable middle ground in this scenario. The SMT is built into the type checker and the refinements are limited to a linearly decidable proof fragment. Dominic Orchard has done some work generalizing the capabilities of these types of refinement by showing that the refinement fragment need to just be a semi-ring structure and the SMT can still resolve. This would cover a large portion of contracts and not impart the development process in large part.
- xmgplays 4y ago
  There is ATS as an example of an imperative language with dependent types.

6gvONxR4sf7o 4y ago

> Unfortunately, people have been focused on the "dynamic" typing (i.e., no type checks) side of things for so long that static checking lags behind in usability The longer I see things like mypy and typescript evolve, I’m actually really glad that people have been focused on gradually typing dynamic languages. As far as I can tell, really useful contracts (or really flexible types) are super burdensome in the most general cases (e.g. `refl` brain twisters in dependent types), but still insanely useful in frequent cases. It reminds me of what people say about static typing’s benefits and burdens. So I’m hoping to see the gradual typing equivalent for contracts and verification. Start with usefulness and add a spectrum of optional safety that the programmer can ignore or use as they see fit. Personally, at least, that would be my ideal scenario.