Champion "Method Contracts"

gafter commented 7 years ago

[ ] Proposal added
[ ] Discussed in LDM
[ ] Decision in LDM
[ ] Finalized (done, rejected, inactive)
[ ] Spec'ed

CyrusNajmabadi commented 2 years ago

I had this exact same conversation 15 years ago trying to explain to C developers why C#,

I'm fine waiting 15 years for the ecosystem to change and for contracts to be mature enough to be worthwhile to adopt into the language itself.

CyrusNajmabadi commented 2 years ago

Let's posit that (incredibly unlikely) the ISO organization decides to change their definition of the calendar,

This information can change all the time. As per above, the need for a shorter minute may come around. This is not at all unlikely.

Furthermore, your approach here depends on when being able to recompile everything in the system since these changes now make your abi incompatible. What do you do if you can't recompile these things? Contracts as API got a dynamic sorry of system like this week just break the world and will be highly unpalatable.

CyrusNajmabadi commented 2 years ago

I do not disagree that it is "expensive" on multiple facets.

If love to see a demonstration of it not being expensive. All the attempts at contracts I've seen (both in practical projects, and in research) have had enormous expenses associated with them.

douglasg14b commented 2 years ago

This discussion seems to have went off the rail, perhaps take datatime things to a discussion? Half of this argument is irrelevant here.

As @Lexcess said:

Even if contracts is a terrible use case for datetime [...], that doesn't prove contracts do not have any value.

The specific use case is probably a good fit for a discussion thread, not here in the champion issue?

CyrusNajmabadi commented 2 years ago

C#/Roslyn seems to have everything needed to do it the easy way

If love to see a demonstration of this. If it is easy, then a fork that demonstrates this should not be hard. However, all the research I've seen that has tried to use c#/.net has not borne it out that this is easy.

CyrusNajmabadi commented 2 years ago

Yes, this breaks the build, but the alternative is releasing a build that errors at runtime.

I think you're stating this as if they are equivalent. If you break the build, it's broken. And that's bad for all the reasons that we care about compat today and are not going to break people. However, if there's a potential for runtime error that can be entirely fine, especially is that runtime error is either rare, or actually will not happen in these deployments.

The latter happens all the time. A lib adds a more restrictive check, but all the data that actually flows into it is fine. Now there is no break. Contrast this with a contract break where now you must actually unbreak things before you can actually proceed.

Elevating contracts to this level is highly problematic. It's one of the strong reasons we don't do things like encode exceptions into our ABI. It's part of what may happen at runtime, and changing it could affect consumers. However, it is enormously costly on an ecosystem to actually go this route, and it virtually guarantees the need for libraries and consumption code to commonly just disable the systems to work and compose in any acceptable fashion.

Lexcess commented 2 years ago

I think you're stating this as if they are equivalent. If you break the build, it's broken. And that's bad for all the reasons that we care about compat today and are not going to break people. ....

To try and at least take this conversation back to the wider case. Let us just assume everything you are worried about is true, a library designer could use contracts at design & debug time, and then choose not to emit them into production builds.

The ability to selectively emit guard code based on various traits (e.g. public surfaces only) or scenarios was one of the key features that attracted me to them in the first place.

CyrusNajmabadi commented 2 years ago

Let us just assume everything you are worried about is true, a library designer could use contracts at design & debug time, and then choose not to emit them into production builds.

This presumes a particular implementation strategy that effectively convinces me there's not need for this to be in the language itself. Perhaps it can be a system that overlays on top of IL to specify a language for constraints. Then different analyzers can validate actual user code against those constraints.

The ability to selectively emit guard code based on various traits (e.g. public surfaces only) or scenarios was one of the key features that attracted me to them in the first place.

This concept came up recently with !!, and it became clear very quickly that this becomes untenable. For example there is no accepted definition on what they public surface area of something is.

Lexcess commented 2 years ago

This presumes a particular implementation strategy that effectively convinces me there's not need for this to be in the language itself. Perhaps it can be a system that overlays on top of IL to specify a language for constraints. Then different analyzers can validate actual user code against those constraints.

That just seems a non-sequitur to me. Should Nullable Reference Types not be a language feature because it has an implementation flag? This thread is for championing the language feature, if you want to raise another thread for an analyzer I would be interested in the proposal.

This concept came up recently with !!, and it became clear very quickly that this becomes untenable. For example there is no accepted definition on what they public surface area of something is.

I could be wrong, but it feels like you have not used the existing Method Contracts implementation. I used these features and do not doubt there were edge cases, but they were robust enough to add value to production code.

CyrusNajmabadi commented 2 years ago

This thread is for championing the language feature,

A very big part of that is even determining if the feature should be done and whether or not alternative approaches would be preferable instead. This fork of the conversation is entirely about that.

CyrusNajmabadi commented 2 years ago

I could be wrong, but it feels like you have not used the existing Method Contracts implementation.

Not only have I used it, but I was on the c# team when we tried to actually use it realistically in production. We had to discontinue the idea for many problems (perf being a particular large one of those). :-)

If things have changed and perf is actually at all acceptable level that allows these systems to scale up to real world codebase sizes effectively, then that would make things more palatable. However, even in my last survey of the state of things (admittedly like 5 years ago), all the contract systems still had major issues here.

Lexcess commented 2 years ago

Not only have I used it, but I was on the c# team when we tried to actually use it realistically in production. We had to discontinue the idea for many problems (perf being a particular large one of those). :-)

Glad I added the caveat about being wrong then! Perf was definitely an issue which is why I would always advocate for a more refined scope of contract options (dropping things like invariants, perhaps only offering pre-conditions to start with etc...).

The reason I said that though, was that your contributions seemed to dismiss what people did find useful about contracts, rather than contribute on how to rework the concept into something that would meet the bar as a language feature. I think most here are realistic about why Method Contracts as it was would never make it.

At a high level I like the idea of describing complex constraints inline in code. Not scattered off in separate types. Not implied by various test suites. Directly in my code. Without contracts we tend to use repetitive inline guard clauses (if you are lucky) and tests, plus we obviously do not have the same guard metadata model for use in API definitions and enforcement.

Obviously, the original implementation had some other cool features (inference for example), but personally I do not consider much from the original implementation to be sacred in the process of getting the concept adopted as a language feature.

So, if I could steer you, it would be towards what would a performant and robust language feature for people who like the concept of contracts look like? As opposed to simply arguing if they should exist at all or be constrained by the flaws and overambition of previous implementations.

acaly commented 2 years ago

Trying to persuade the team some feature is good or important to you is useless. They have said above that they would like to let you wait for 15 years.

One example is the recent "file private" visibility, which is a feature similar to what had been proposed by community years ago, but is only discussed seriously recently when the c# runtime team found it useful.

CyrusNajmabadi commented 2 years ago

The reason I said that though, was that your contributions seemed to dismiss what people did find useful about contracts,

I def can appreciate what people find useful. But at the same time, making a language change means we have to have practical solutions here. :-)

CyrusNajmabadi commented 2 years ago

They have said above that they would like to let you wait for 15 years.

Right. I don't get what's contentious about that. If the feature takes 15 years until it's viable then we shouldn't be shipping earlier.

CyrusNajmabadi commented 2 years ago

but is only discussed seriously

This feature has been discussed seriously.

when the c# runtime team found it useful.

This is not the case. The discussion was advanced because a reasonable proposal was put forth that actually handled a whole host of concerns that are needed.

We have limited resources, so having a realistic proposal or forth that goes in depth and works to balance many concerns, addresses costs, and thinks about how it can be expanded in the future, ends up being something that here attention enough from an ldm member to champion.

Clockwork-Muse commented 2 years ago

The latter happens all the time. A lib adds a more restrictive check, but all the data that actually flows into it is fine. Now there is no break. Contrast this with a contract break where now you must actually unbreak things before you can actually proceed.

In context, I was speaking about a more restrictive check that would be triggered by an application constant. That is, the data that flowed in would never be fine, so the build would be broken regardless of whether it was due to a compile-time contract or the type's runtime check on application load.

It's one of the strong reasons we don't do things like encode exceptions into our ABI.

... I mean, I'd like checked exceptions too, if I could get them (But that would require quite a bit wider changes to the exception ecosystem, a la Midori).

CyrusNajmabadi commented 2 years ago

So, if I could steer you, it would be towards what would a performant and robust language feature for people who like the concept of contracts look like?

I genuinely don't know. I've seen many attempts at this that have not been viable. So my default position here is that efforts would likely be better allocated elsewhere.

I do think if someone in the community, or other venues (like academia) can prove this out, then that would certainly make things much more likely.

I personally have no clue how to pull this off. I wish I did! :-)

CyrusNajmabadi commented 2 years ago

so the build would be broken regardless of whether it was due to a compile-time contract or the type's runtime check on application load.

I think the challenge is more at the edges. Say one API says it generates values from the set S, and one API says it takes values from the same set. But then the second API changes to {S-1}. Now you have a contract break. However, it's entirely possible that in reality that single value that is not accepted is not actually ever generated by the first API (it's just marked that way as a reasonable, slightly broader, contract).

This would now break with a contract incongruity, despite very possibly not being an actual problem for these libs. That's why I don't want to actually encode this as an abi. I'd far prefer it as just a relaxed analysis system that layers on top.

This is also much more palatable as such analysis is not encumbered by the same compat rules we have. A different owner can decide a different set of rules and compat decisions that make sense to them.

CyrusNajmabadi commented 2 years ago

... I mean, I'd like checked exceptions too, if I could get them (But that would require quite a bit wider changes to the exception ecosystem, a la Midori).

I'd love to see a design there that can work in practice. For example how would a linq system work with checked exceptions? How do you support passing delegates to things when exceptions are part of your signatures?

Clockwork-Muse commented 2 years ago

This would now break with a contract incongruity, despite very possibly not being an actual problem for these libs. That's why I don't want to actually encode this as an abi. I'd far prefer it as just a relaxed analysis system that layers on top.

I don't think I really disagree with this concern. What I'm wondering about here is whether we could get the runtime/JIT in on the act for stuff like this. That is, the ABI has the signatures, and at load/JIT time it compares them - if they're compatible it discards any checks, otherwise it emits the necessary checks to throw them as runtime errors. As a rough concept, this also allows it to work with libraries that haven't been compiled with the necessary information, since it would be considered as having no validation.

I'd love to see a design there that can work in practice. For example how would a linq system work with checked exceptions? How do you support passing delegates to things when exceptions are part of your signatures?

From the look of things, Midori would have done something like

public static class Enumerable 
{
    public static TResult Select<TSource, TResult, throws E>(this IEnumerable<TSource> source, Func<TSource, TResult, E> selector) E
    {
        foreach (TSource element in source)
        {
            yield return try selector(element);
        }
    }
}

// I don't think you needed to do anything at the call site if you couldn't throw a non-abandonment exception?  Blog slightly unclear here.
// Something like normal.
var n = new [] { 1, 2, 3 }.Select(n => n + 1);
var n = try new [] { 1, 2, 3 }.Select(n => throw new IOException());

... although probably IOException is the only exception that might be reasonably be needed to be used in such a situation - most of the others causing abandonment, and not meaning to be caught.

MovGP0 commented 2 years ago

Day can never be over 31

Month must be between 1 and 12

Second must be between 0 and 59 (in the case of TimeSpan, -59 and 59)

etc.

I think you should check out this:

Falsehoods programmers believe about time

Or for a more complete list:

Awesome Falsehood

Rekkonnect commented 2 years ago

I think you should check out this:

Falsehoods programmers believe about time

Yeah I was already told that time is far more disgusting than I thought. Not part of the discussion.

Part of the discussion now:

I genuinely don't know. I've seen many attempts at this that have not been viable. So my default position here is that efforts would likely be better allocated elsewhere.

Internal attempts in the C# team? Or general attempts like other languages (Dafny is one that comes to my mind).

I do think if someone in the community, or other venues (like academia) can prove this out, then that would certainly make things much more likely.

What kind of performance are we talking about? Compilation or runtime? Because compile-time contracts are what I have been dreaming of, eliminating runtime checks, further improving performance in the process, in alignment with runtime support and JIT optimizations.

Lexcess commented 2 years ago

The discussion was advanced because a reasonable proposal was put forth that actually handled a whole host of concerns that are needed.

I am not sure if I have seen this proposal, nor the remaining concerns that meant it didn't pass muster. Could you link or copy both here?

acaly commented 2 years ago

The discussion was advanced because a reasonable proposal was put forth that actually handled a whole host of concerns that are needed.

I am not sure if I have seen this proposal, nor the remaining concerns that meant it didn't pass muster. Could you link or copy both here?

Actually I don't think the proposal I was talking about ("file private" visibility, as I don't want to create a reference I would not provide a link here) can be considered "a reasonable proposal put forth" at the time most discussion happened. Most of the content was added later.

There are many examples in this repo that someone from the community wrote a much longer proposal and got no more than 2 replies. It is not a very good experience to spend time writing proposals here. As I said, it is very hard to persuade the team to do or not to do something. Such work is better left to themselves.

Lexcess commented 2 years ago

The discussion was advanced because a reasonable proposal.

Apologies, I misunderstood. From the reply I thought there was such a proposal for contracts.

marinasundstrom commented 2 years ago

I created a proposal for a compile-time Code Contracts based on attributes that can be analyzed as part of the development experience.

https://github.com/marinasundstrom/CodeContractsTest

The analyzer is not there. But I give hints on what kind of errors there could be.

There is also a syntax proposal.

I know that someone has already been experimenting with implementing it into the compiler.

Genbox commented 2 years ago

There is also a syntax proposal.

I personally like it. Just thinking about having IntelliSense and compile-time checking of the contract specs makes me all giddy. I think both approaches should be implemented - that way the language extension could compile into the attribute, and an analyzer on the consumer's side could check the contract.

For example:

public int CalculateLevel(int userLevel)
    requires userLevel >= 0,
    ensures result >= 100
{
    int systemLevel = 100;
    return systemLevel + userLevel;
}

This would compile into a C# backward-compatible spec with attributes:

[Ensures("result >= 100")]
public int CalculateLevel([Requires(">=0")]int userLevel)
{
    int systemLevel = 100;
    return systemLevel + userLevel;
}

As such, an analyzer could easily traverse the AST, extract the attributes and run the SMT solver.

marinasundstrom commented 2 years ago

@Genbox Yes. This is the first step. Building the infrastructure.

There are a lot of advanced patterns to be dealt with (like str.Length < 10), but someone should at least try the simpler ones before ruling out its a bad idea.

An analyzer plugin can be written quite easily to test the concept. I did create a project for attempting that in my repo.

When it comes to the language syntax, I remember someone a long time ago (I think in this issue) posting a concept of implementing it in Roslyn.

From my repo:

// CS1234: Argument does not satisfy requirement: arg < 42
// CS1235: InvalidOperationException is unchecked.
var result = DoSomething(42);
                         ~~

// "result" is marked as satisfying > 0

// CS1234: Argument does not satisfy requirement: input < 0
Foo(result);
    ~~~~~~

[Throws(typeof(InvalidOperationException))]
[return: Ensures("return > 0")]
int DoSomething([Requires("arg >= 0"), Requires("arg < 42")] int arg)
{
    if(arg == 10)
    {
        throw new InvalidOperationException();
    }
    return arg;
}

void Foo([Requires("input < 0")] int input)
{

}

Another example:

File file = new ();

// "name" is satisying Length =< 50;
var name = file.FileName;

// This means that you get an error or warning

// CS1234: Argument does not satisfy requirement: fileName.Length >= 60
ReadFile(name);
         ~~~~

void ReadFile([Requires("fileName.Length >= 60")] string fileName)
{

}

class File 
{
    public string FileName 
    {
        [return: Ensures("return.Length =< 50")]
        get;
    } = null!;
}

Genbox commented 2 years ago

@marinasundstrom I discussed the problem of second-order/derived values with Professor Joseph Kiniry back in 2011. From what I remember, we came up with 5 different solutions, but they were in the context of "code correctness", and as such, even the body of a method had to follow the contract (and invariants would ensure the state of objects).

For example, a "full contract" solution means that the code is seen as a proof that has to be QED before it compiles. For example:

public int Add(int val1, int val2)
   ensures result <= int.MaxValue
{
   //This line would result in an exception when checked mode is turned on
   return val1 + val2; // <- this fails the contract. int.MaxValue + int.MaxValue is larger than int.MaxValue
}

public int Add(int val1, int val2)
   ensures result <= int.MaxValue
{
    Math.Clamp(val1, int.MinValue, (int.MaxValue -1) / 2); // <- can also be a require contract
    Math.Clamp(val2, int.MinValue, (int.MaxValue -1) / 2); // <- can also be a require contract
    return val1 + val2; // <- This now passes
}

This kind of contract is amazing for correctness, but difficult to implement, which is why Code Contracts had Contract.Require() on the incoming data, then normal data validation checks, and finally Contract.Assume() to satisfy the SMT constraints.

However, if we focus on pure API contracts and the second-order/derived values, only 2 solutions seemed to be viable. All examples below are a "require contract". Imagine [Requires("example here")].

Solution A: Explicit naming. That is the solution you have in your example. Example: "filename.Length <= 40"

Pro: Easy to understand. Follows conventional thinking of C# developers
Pro: Everything can be represented with the same structure. Example: "collection.Any(x=> x.Length == 4)"
Con: Requires the spec analyzing (dynamic) code to understand arbitrary code. This is where contracts would overlap with runtime checks as you would need to know the value of "collection.Any(x=> x.Length == 4)" before you run the SMT solver.

Solution B: Macros. Imagine you have a macro to calculate the length of types. Example: "length(filename) <= 40"

Pro: It is explicitly defined that we are working with the length of a structure. It can be any collection.
Pro: While it looks like it runs at runtime, it does not. It is like changing the type of filename from string to stringOfMaxLength40. When the developer gives it "SomePath" it works just fine because it gets compiled to a stringOfMaxLength40 type. However, if it is longer than 40 characters, it will not compile to the type and compilation fails. Of course, like any other static analysis, it only works on constant data or when we can assume/require to satisfy the constraint
Con: Requires developers to learn the macros. length(), max(), min() is just a subset of the required macros.
Con: For length() to work on an arbitrary type, the developer would need to implement an interface. Code is not always available to do so.

Clockwork-Muse commented 2 years ago

but someone should at least try the simpler ones before ruling out its a bad idea.

The patterns or exact conditions representable aren't really the problem.

The biggest problem is the ecosystem - defining the compatibility of the ABI, dealing with NuGet packages, loading libraries with potentially conflicting/no info.... This isn't much of an issue if you commonly recompile the entire world (you only use the runtime, plus one or two updated package, to write an application). It's a major challenge when trying to deal with all the existing libraries out there, especially if they're stable and don't otherwise need to be recompiled (or can't, for any number of reasons).

marinasundstrom commented 2 years ago

@Clockwork-Muse Yes, that is why I propose the attributes approach just like with Nullable reference types. Letting you opt-in or out.

marinasundstrom commented 2 years ago

@Genbox Yea. I think there is a limitation to what we, realistically, can check and what expressions to allow.

We can mainly assure that locals and fields of primitive values are set to a certain value. Not evaluate that methods yield specific results.

There is a special case to this approach that I proposed:

The string literal “Foo” will yield a string instance that has a Length (3) annotated to it. It will help us make assumptions about that property.

After a local variable has received an instance of a string with a certain Length, I argue it should Ensure that any possible future assignments adhere to the same specification. The variable now has an Ensure attached to itself.

Genbox commented 2 years ago

@Clockwork-Muse

defining the compatibility of the ABI

That is not an issue, it is a feature. No really.

If a developer says "i need this input to be [1..10", but you have always given it 11 and it worked just fine, then you are relying on the developers good graces where he probably did something like if (val > 10) val = 10; //damn users.

When he updates the code with a contract that says requires val >= 0 && val <= 10 and your code suddenly no longer compiles, that is a good thing - you had a bug. Fix it to satisfy the contract.

potentially conflicting

Conditions just needs to be satisfied, so if one contract says requires val >= 0 && val <= 10 and another says requires val >= 0 && val <= 9, if the value is 5, both are satisfied. So what happens when the value is 10?

Well, not much. Your application won't compile, but the author declared his library won't work with a value of 10 anyway, so don't give it 10 or have them update their contracts. Today we mostly hope that it "just works", but if a library author explicitly declare that he does not support a value of 10, I'd much rather want to know it a compile-time than suddenly at run-time.

But lets say 10 is perfectly valid and the library author won't update his contract, then it shouldn't be that difficult to add an exception to the SMT solver so that particular check is not included. For example:

//Your code
static void Main()
{
   // Example 1 - Ignore contract for specific value
   Calculate(11!); // <- usually fails, but ! denotes that it is ignored (like with nullability)

   // Example 2 - Pragma warning disabled. Might disable multiple contracts on this line
   #pragma warning disable XXX
   Calculate(11); // <- usually fails, but pragma compiler directive ignores it

   // Example 3 - Explicit exclusion for code contracts
   #DisableContract(val)
   Calculate(11); // <- usually fails, but not for 'val' has it has been disabled
}

//Library code
public int Calculate(int val)
   requires val >= 0 and <= 10
{ }

@marinasundstrom have you thought about how to exclude one single requirement vs. disabling the analyzer for a whole line?

marinasundstrom commented 2 years ago

@Clockwork-Muse “ABI” will always break when you recompile. That is what happens all the time.

But at least it will not cause too much havoc, since this does not change the fundamentals of the CLR or the metadata. It is an opt-in compiler feature.

@Genbox No, I have not. That is worth thinking about.

We probably need to recognize parts that are not annotated too. Warn about passing a value from a source without a specification. And a way to tell the compiler that its OK.

Clockwork-Muse commented 2 years ago

Yes, that is why I propose the attributes approach just like with Nullable reference types. Letting you opt-in or out.

The fact that they're attributes don't make them optional.

That is not an issue, it is a feature. No really.

This assumes that everything is getting recompiled, and for that, I agree with you. That is not the case for the wider ecosystem, especially when first released. People will want to be able to compile an app/library that uses/publishes contracts but depends on a library that doesn't. That's the harder part of the ABI/compat problem. In particular...

Conditions just needs to be satisfied

Assume that the conditions are from libraries that you pull in as dependencies, so you can't recompile the code. That's the actual issue here.

“ABI” will always break when you recompile. That is what happens all the time.

It doesn't actually. If this were the case, you couldn't update transitive dependencies until any other libraries using it were also update. Major library teams spend a lot of effort ensuring that they can publish patched binaries that are usable without recompiling other things that depend on them. It would mean that Windows Update would break all your applications.

Part of the "hard stuff" for this feature is even figuring out whether adding contracts at all would be a breaking change or not.

rwv37 commented 1 year ago

"I'm very curious about those edge cases."

There's an interesting page https://nodatime.org/2.2.x/userguide/trivia on the NodaTime website about stuff like this.

On 3/19/2022 4:48 PM, AlFas wrote:

There have been months that have had 32 days.

Minutes can be 61 seconds long.
I'm very curious about those edge cases.
your programming language may not allow you to represent things
that are necessary.
Either way, there can be similar constraints; I'm not the one to design the APIs, i.e. on dates. Whoever wrote the date APIs will take this feature seriously into consideration before applying it, let alone the how.

— Reply to this email directly, view it on GitHub https://github.com/dotnet/csharplang/issues/105#issuecomment-1073078763, or unsubscribe https://github.com/notifications/unsubscribe-auth/AB5RDQLK6YNK5RNNTG45CPTVAY4QHANCNFSM4DAESNBA. Triage notifications on the go with GitHub Mobile for iOS https://apps.apple.com/app/apple-store/id1477376905?ct=notification-email&mt=8&pt=524675 or Android https://play.google.com/store/apps/details?id=com.github.android&referrer=utm_campaign%3Dnotification-email%26utm_medium%3Demail%26utm_source%3Dgithub.

You are receiving this because you are subscribed to this thread.Message ID: @.***>

dotnet / csharplang

Champion "Method Contracts" #105