5 ms·

>> A serious take on a contract-based language Ada has design-by-contract as part of the language: https://learn.adacore.com/courses/intro-to-ada/chapters/con

>> A serious take on a contract-based language Ada has design-by-contract as part of the language: https://learn.adacore.com/courses/intro-to-ada/chapters/contracts.html https://learn.adacore.com/courses/intro-to-ada/chapters/cont... Since Ada is used for safety-critical systems programming you could argue that it is very serious about it. >> And tool integration! One of the coolest things Eiffel sorta did was use contracts to infer tests. If you have contracts, you can use a fuzzer to get integration tests for free. How about tools that extend design-by-contract to formal verification? https://learn.adacore.com/courses/intro-to-spark/chapters/01_Overview.html# https://learn.adacore.com/courses/intro-to-spark/chapters/01... SPARK is limited to a subset of Ada, so it is not without limitations, but it can be very useful depending on what you are trying to do.

ainar-g 4y ago
The D programming language, too. https://dlang.org/spec/function#contracts https://dlang.org/spec/function#contracts
- bvoq 4y ago
  +1 on D. It even has contracts for members.
DoingIsLearning 4y ago
If Adacore had published a full featured free compiler for students/universities by the time Ada 95 standard was published, I am sure that Ada could have occupied the space C++ takes today. Mostly what Ada lacks is not the features but the comunity effect, we saw that when comparing feature parity with C++ and we see that again when comparing feature parity with Rust. There are a lot of briliant features and tooling in Ada, but unless there is a community effect (or a gigantic industry sponsor e.g. golang) it is difficult to convince people to switch over. I can't remember who said it so I will paraphrase, the best language/target to program in is whatever your friends/colleagues are using.
- thesuperbigfrog 4y ago
  >> If Adacore had published a full featured free compiler for students/universities by the time Ada 95 standard was published, I am sure that Ada could have occupied the space C++ takes today. Agreed. If there had been more free (gratis) or low-cost Ada compilers at that time Ada would be far less niche than it is today. There is increased interest in Ada today thanks to Rust. There is also interplay between Rust and Ada/SPARK features with Rust getting some Ada features and SPARK getting some Rust features. Ferrous Systems is working with AdaCore on the Ferrocene Language Specification to formally document the Rust subset that Ferrocene will use: https://ferrous-systems.com/ferrocene/ https://ferrous-systems.com/ferrocene/ https://ferrous-systems.com/blog/ferrocene-language-specification/ https://ferrous-systems.com/blog/ferrocene-language-specific... It is exciting to see Rust mature so it can one day be used in safety-critical work.
  - the_only_law 4y ago
    This seems to be a common theme among certain languages, software, etc. from the 90s. I've heard similar things about Smalltalk.
    - igouy 4y ago
      Long before the digital era that common theme would have been expressed as — Don't look a gift horse in the mouth.
- toolslive 4y ago
  Yup, also the commercial ADA IDEs were brilliant, even compared to Borland, but o-so-expensive.
- augustk 4y ago
  > If Adacore had published a full featured free compiler for students/universities by the time Ada 95 standard was published, I am sure that Ada could have occupied the space C++ takes today. The same can be said about Eiffel.
hwayne 4y ago
Forgetting about SPARK was a big whoops for me. (Lots of formal verification languages are based on contracts, like SPARK, Frama-C, and Dafny. I'm interested in uses for contracts that aren't just formal verification, though!)
- thesuperbigfrog 4y ago
  >> I'm interested in uses for contracts that aren't just formal verification, though! Ada 2012 design-by-contract features aren't just for formal verification, they can be used in a general purpose way similar to Eiffel: https://learn.adacore.com/courses/intro-to-ada/chapters/contracts.html https://learn.adacore.com/courses/intro-to-ada/chapters/cont... Can you elaborate a bit more about the wanted features for a language with semantic relations?
  - hwayne 4y ago
    An example off the top of my head would be writing a serializer/deserializer pair and explicitly saying they are inverses of each other, as opposed to having to implicitly say that in a round-trip property test. Another idea would be being able to say that two data representations are isomorphic under a given transformation, so I can define a function for one transformation and call it on the other. I don't know how useful this would be in practice, but it seems interesting to me!
    - thesuperbigfrog 4y ago
      >> writing a serializer/deserializer pair and explicitly saying they are inverses of each other, as opposed to having to implicitly say that in a round-trip property test. That capability would be very useful. There are many cases where I have had to define serialization and deserialization functions for numerous objects and had to create so much "boilerplate" unit test code like you describe. It made me wish I was using a Lisp with built-in reader and printer functions. >> being able to say that two data representations are isomorphic under a given transformation, so I can define a function for one transformation and call it on the other. This strikes me as very Haskell-ish, but could be quite useful to ensure certain properties or invariants.
ajdude 4y ago
When I read "contract-based language"I immediately thought of Ada. I could be wrong but I think SPARK is incorporated into the Ada 2022 standard at this point, it could really be thought of as part of the language. It's the furthest thing from a "dynamically typed language" but it can probably also check the "math" requirement here too.
ibains 4y ago
Its not public language, but at Risk Management Systems, I worked on Contract Definition Language- an external DSL for computable insurance, re-insurance contracts. This was used to simulate insurance losses when catastrophic events happen (earthquake, hurricane)
- fernirello 4y ago
  Any good reference for that CDL? The idea seems quite useful for what I'm working on. All I found is a wishy-washy doc with poorly chosen examples [0] [0] https://www.riskdataos.org/html/HelpCenter/Content/CDL/CDL_Semantics_Intro.htm https://www.riskdataos.org/html/HelpCenter/Content/CDL/CDL_S...
  - occamrazor 4y ago
    RMS never played nice on interoperability. I wouldn’t bet on the CDL to become a useful standard, because it is under-powered, under-specified and stagnant. The “open” alternative is OASIS. Their Open Exposure Data standard [1] is complete and supported by many industry participants. Unfortunately it’s a database based format, rather than a text based DSL, but still betterthan the alternatives. [1] https://github.com/OasisLMF/OpenDataStandards/tree/master/OpenExposureData/Docs https://github.com/OasisLMF/OpenDataStandards/tree/master/Op...
    - fernirello 4y ago
      Thank you! I wasn't aware of OASIS. Reading up now.
kaba0 4y ago
Java has a similar “extension” as well: https://en.m.wikipedia.org/wiki/Java_Modeling_Language https://en.m.wikipedia.org/wiki/Java_Modeling_Language
dude12344 4y ago
Also Nim has contracts and supports formal proofing: https://nim-lang.org/docs/drnim.html https://nim-lang.org/docs/drnim.html
- elcritch 4y ago
  A more practical one might be this contracts library https://github.com/Udiknedormin/NimContracts https://github.com/Udiknedormin/NimContracts
hinkley 4y ago
Better still would be to take progressively typed languages, combined with contracts and property-based testing, and iterate toward a more precise contract for all of your code whenever it became necessary or whenever you got bored. What are the consequences of deciding that no Foo's are allowed to be red? Hmm, that's interesting/unintended... The main difficulties with statically typed languages seem to be both 1) quickly arriving at a workable prototype, and 2) dealing with the consequences of regrettable decisions made early on. Those two being in tension contributes a lot of drama, and not just in analysis paralysis.
tonyhb 4y ago
Similarly, Ruby had RDL - which implemented pre/post contracts and type checking prior to Sorbet. It was actually pretty nice, if slow. https://github.com/tupl-tufts/rdl https://github.com/tupl-tufts/rdl
miclill 4y ago
Fuzion has contracts as well: https://flang.dev/tutorial/pre_post_conditions https://flang.dev/tutorial/pre_post_conditions https://github.com/tokiwa-software/fuzion https://github.com/tokiwa-software/fuzion Disclaimer, I work in the Fuzion team.

ainar-g 4y ago

The D programming language, too. https://dlang.org/spec/function#contracts https://dlang.org/spec/function#contracts

bvoq 4y ago
+1 on D. It even has contracts for members.

DoingIsLearning 4y ago

If Adacore had published a full featured free compiler for students/universities by the time Ada 95 standard was published, I am sure that Ada could have occupied the space C++ takes today. Mostly what Ada lacks is not the features but the comunity effect, we saw that when comparing feature parity with C++ and we see that again when comparing feature parity with Rust. There are a lot of briliant features and tooling in Ada, but unless there is a community effect (or a gigantic industry sponsor e.g. golang) it is difficult to convince people to switch over. I can't remember who said it so I will paraphrase, the best language/target to program in is whatever your friends/colleagues are using.

thesuperbigfrog 4y ago
>> If Adacore had published a full featured free compiler for students/universities by the time Ada 95 standard was published, I am sure that Ada could have occupied the space C++ takes today. Agreed. If there had been more free (gratis) or low-cost Ada compilers at that time Ada would be far less niche than it is today. There is increased interest in Ada today thanks to Rust. There is also interplay between Rust and Ada/SPARK features with Rust getting some Ada features and SPARK getting some Rust features. Ferrous Systems is working with AdaCore on the Ferrocene Language Specification to formally document the Rust subset that Ferrocene will use: https://ferrous-systems.com/ferrocene/ https://ferrous-systems.com/ferrocene/ https://ferrous-systems.com/blog/ferrocene-language-specification/ https://ferrous-systems.com/blog/ferrocene-language-specific... It is exciting to see Rust mature so it can one day be used in safety-critical work.
- the_only_law 4y ago
  This seems to be a common theme among certain languages, software, etc. from the 90s. I've heard similar things about Smalltalk.
  - igouy 4y ago
    Long before the digital era that common theme would have been expressed as — Don't look a gift horse in the mouth.
toolslive 4y ago
Yup, also the commercial ADA IDEs were brilliant, even compared to Borland, but o-so-expensive.
augustk 4y ago
> If Adacore had published a full featured free compiler for students/universities by the time Ada 95 standard was published, I am sure that Ada could have occupied the space C++ takes today. The same can be said about Eiffel.

hwayne 4y ago

Forgetting about SPARK was a big whoops for me. (Lots of formal verification languages are based on contracts, like SPARK, Frama-C, and Dafny. I'm interested in uses for contracts that aren't just formal verification, though!)

thesuperbigfrog 4y ago
>> I'm interested in uses for contracts that aren't just formal verification, though! Ada 2012 design-by-contract features aren't just for formal verification, they can be used in a general purpose way similar to Eiffel: https://learn.adacore.com/courses/intro-to-ada/chapters/contracts.html https://learn.adacore.com/courses/intro-to-ada/chapters/cont... Can you elaborate a bit more about the wanted features for a language with semantic relations?
- hwayne 4y ago
  An example off the top of my head would be writing a serializer/deserializer pair and explicitly saying they are inverses of each other, as opposed to having to implicitly say that in a round-trip property test. Another idea would be being able to say that two data representations are isomorphic under a given transformation, so I can define a function for one transformation and call it on the other. I don't know how useful this would be in practice, but it seems interesting to me!
  - thesuperbigfrog 4y ago
    >> writing a serializer/deserializer pair and explicitly saying they are inverses of each other, as opposed to having to implicitly say that in a round-trip property test. That capability would be very useful. There are many cases where I have had to define serialization and deserialization functions for numerous objects and had to create so much "boilerplate" unit test code like you describe. It made me wish I was using a Lisp with built-in reader and printer functions. >> being able to say that two data representations are isomorphic under a given transformation, so I can define a function for one transformation and call it on the other. This strikes me as very Haskell-ish, but could be quite useful to ensure certain properties or invariants.

ajdude 4y ago

When I read "contract-based language"I immediately thought of Ada. I could be wrong but I think SPARK is incorporated into the Ada 2022 standard at this point, it could really be thought of as part of the language. It's the furthest thing from a "dynamically typed language" but it can probably also check the "math" requirement here too.

ibains 4y ago

Its not public language, but at Risk Management Systems, I worked on Contract Definition Language- an external DSL for computable insurance, re-insurance contracts. This was used to simulate insurance losses when catastrophic events happen (earthquake, hurricane)

fernirello 4y ago
Any good reference for that CDL? The idea seems quite useful for what I'm working on. All I found is a wishy-washy doc with poorly chosen examples [0] [0] https://www.riskdataos.org/html/HelpCenter/Content/CDL/CDL_Semantics_Intro.htm https://www.riskdataos.org/html/HelpCenter/Content/CDL/CDL_S...
- occamrazor 4y ago
  RMS never played nice on interoperability. I wouldn’t bet on the CDL to become a useful standard, because it is under-powered, under-specified and stagnant. The “open” alternative is OASIS. Their Open Exposure Data standard [1] is complete and supported by many industry participants. Unfortunately it’s a database based format, rather than a text based DSL, but still betterthan the alternatives. [1] https://github.com/OasisLMF/OpenDataStandards/tree/master/OpenExposureData/Docs https://github.com/OasisLMF/OpenDataStandards/tree/master/Op...
  - fernirello 4y ago
    Thank you! I wasn't aware of OASIS. Reading up now.

kaba0 4y ago

Java has a similar “extension” as well: https://en.m.wikipedia.org/wiki/Java_Modeling_Language https://en.m.wikipedia.org/wiki/Java_Modeling_Language

dude12344 4y ago

Also Nim has contracts and supports formal proofing: https://nim-lang.org/docs/drnim.html https://nim-lang.org/docs/drnim.html

elcritch 4y ago
A more practical one might be this contracts library https://github.com/Udiknedormin/NimContracts https://github.com/Udiknedormin/NimContracts

hinkley 4y ago

Better still would be to take progressively typed languages, combined with contracts and property-based testing, and iterate toward a more precise contract for all of your code whenever it became necessary or whenever you got bored. What are the consequences of deciding that no Foo's are allowed to be red? Hmm, that's interesting/unintended... The main difficulties with statically typed languages seem to be both 1) quickly arriving at a workable prototype, and 2) dealing with the consequences of regrettable decisions made early on. Those two being in tension contributes a lot of drama, and not just in analysis paralysis.

tonyhb 4y ago

Similarly, Ruby had RDL - which implemented pre/post contracts and type checking prior to Sorbet. It was actually pretty nice, if slow. https://github.com/tupl-tufts/rdl https://github.com/tupl-tufts/rdl

miclill 4y ago

Fuzion has contracts as well: https://flang.dev/tutorial/pre_post_conditions https://flang.dev/tutorial/pre_post_conditions https://github.com/tokiwa-software/fuzion https://github.com/tokiwa-software/fuzion Disclaimer, I work in the Fuzion team.