Follow-up idea: Design by Contract

[zmughal]

Per a discussion on Facebook, I wrote the following as possible way to extend the idea of checks to the idea of contracts as defined by the Eiffel programming language:

• Eiffel language created the concept of Design by Contract and it is a core part of the language design. https://www.eiffel.org/doc/eiffel/ET-_Design_by_Contract_%28tm%29%2C_Assertions_and_Exceptions. They unify a lot of different specifications of what a method does/guarantees into a single approach.

• Ada has particular subsets/implementations that use Design by Contract in order use a prover to formally verify that the code follow certain kinds of contracts https://en.wikipedia.org/wiki/SPARK_(programming_language), https://archive.fosdem.org/2021/schedule/event/safety_opensource_ada_contracts/.

I understand if this is not within the scope of the MVP and have no idea how difficult this would be to do, but it would be nice to be open to this possibility. It would be nice if there were sets of these contracts as libraries that could help with, say, making sure code is portable across different OSes or that thread-unsafe constructs are used properly.

I know that there are libraries that implement some of these contract ideas on CPAN which means it is possible to add these dynamically to the language.

[zmughal]

Copy of some of my notes about what is on CPAN:

• assertion / DbC
  • https://metacpan.org/pod/Sub::Contract
  • https://metacpan.org/pod/Class::DbC
  • https://metacpan.org/pod/Class::Contract
  • https://metacpan.org/pod/Attribute::Contract
  • https://metacpan.org/pod/Sub::Assert::Nothing
  • https://metacpan.org/pod/LIVR::Contract
  • https://metacpan.org/pod/MooseX::Contract
  • https://metacpan.org/pod/Class::Agreement
  • https://metacpan.org/pod/Assert::Refute
  • https://metacpan.org/pod/assertions
  • https://metacpan.org/pod/Generic::Assertions
  • https://metacpan.org/pod/Devel::Assert
  • https://metacpan.org/pod/Assert::Conditional
  • https://metacpan.org/pod/Carp::Assert::More
  • https://metacpan.org/pod/PerlX::Assert
• interface
  • https://metacpan.org/pod/Function::Interface
  • https://metacpan.org/pod/Role::Declare

[zmughal]

Worth looking at other languages that support this https://en.wikipedia.org/wiki/Design_by_contract#Language_support and in particular, Java, which has many including https://en.wikipedia.org/wiki/Java_Modeling_Language.

[zmughal]

Indicating what exceptions can be thrown and under what conditions can also be part of the contract.

[zmughal]

I see the spec has VOID. This might also need to be added to functions such as exit() and whenever a sub can die (throw an exception) though VOID is more about context so maybe that concept should not be overloaded? Scala uses Unit and Nothing for these cases, https://www.scala-lang.org/api/current/scala/sys/index.html#exit(status:Int):Nothing. I'm not really sure about this one.

[druud]

See also (the old) https://metacpan.org/pod/Class::Contract

[happy-barney]

Let's rename this discussion to Follow-up idea - Design by Contract to not scare people too early :-)

[zmughal]

Done!

[Ovid]

I'm sorry I haven't responded earlier. This has been a very busy month for me. Rather than juggle too many things, I put some balls down.

That being said, now that I'm responding, I'm in an awkward state. Specifically, Damian and I have had Design by Contract (DBC) discussions before, but these were parts of private conversations we had, with no expectation of them going public, so I can't share everything, but they were generally along the lines of:

• Me: "I have a bad idea."
• Damian: "Yes, you do."

And then he'd kindly share with me a careful explanation of why my idea was bad. Design by Contract (DbC) was one of these discussions. DbC was not the bad thing, but I had a spectacularly bad idea about the implemementation of a related idea and Damian had to talk me off the ledge (though I was taking inspiration from the Beta programming langauge at the time, which probably explains why my idea was so bad). That conversation, however, sparked some ideas which led to the discussion of DbC and different approaches by different languages.

What I can say about our conversation is that DbC works well in the context of Corinna, which was the crux of the discussion. DbC handles pre- and post-conditions, input and output data constraints, invariants, exceptions, etc., and is basically what it says on the tin: it's a contractual software guarantee for an exposed bit of software. It's also a heck of a lot of overhead and DbC systems are often only used in testing or development, but not on production, so there needs to be a way to ensure that not only are they easy to disable. There are also plenty of tricky bits with class composition, such as respecting Liskov, which contracts could theoretically verify, but many languages get this wrong.

In short, considering DbC is great, but DbC for Oshun would be using a AK-47 Type 2A gas-operated assault rifle for killing a mosquito. It'll do the job, but I just swat 'em with my hand. Your mileage may vary.

You also mention assertions and those seem a great fit here, but I'd probably open up any DbC discussion on Corinna because that is well within the scope of future work.

For the DbC, one thing that struck me as interesting is that so many people have taken swipes at implementing DbC in Perl, but I can't find any evidence that anyone uses existing systems. I don't know if that's because they find the implementations clumsy or because they just don't like DbC. Or it could be that Perl devs do such a terrible job of writing OO code that it would be, um, hard to create a contract for many classes.

However, for Perl+Corinna, here are some thoughts for that discussion:

• Pre and post conditions could be phasers (but how do we avoid subverting Liskov?)
• The incoming and outgoing data checks would be ... Oshun!
• Exceptions might need to be native in Perl and that's likely to be tightly coupled with native (c-level) stack traces
• Invariants ... definitely would need some deep thought on this. Where are clean examples of them being needed?
• Integration withe MOP for automated test case generation

Exceptions+Stack Traces would be a bit of a blocker. Without having them native, I suspect it would be awfully hard to specify that method foo() throws IO { ... } and expose that cleanly in a contract. That being said, one could punt on them for a first pass at DbC, though that would be disappointing.

[happy-barney]

therefor we renamed it as follow-up idea ... summarize links to other systems, talk about it. Quoting book I'm currently reading: invention is nearly impossible without knowledge.

And definitely, this is beyond scope of simple data checks ... but data checks are significant part of contracts.