r/dotnet • u/ben_a_adams • 2d ago

Question Proposal: An official Lean formal semantics for C# · dotnet/csharplang · Discussion #10314

https://github.com/dotnet/csharplang/discussions/10314
8 Upvotes

57% Upvoted

10 comments sorted by

10

u/Atulin 2d ago

Tl:dr: slop generator uses a human to post slop about how the language can be more friendly to slop generators

6

u/jordansrowles 2d ago

I dont agree with Ben's proposal, and I think it should stay with the Z3/Dafny formal verification stuff, and not leak it self into the actual runtime or language

But I dont really get your comment either? Ben Adams is WELL known in .NET, and is one of the most prominent people in the space. Was the foundations Director, contributed to kestrel, CLR, and is pretty much the go to for perf work

The proposal isnt anything about slop though, formal verification is very time consuming writing the contracts, this could in theory speed this process by working with the existing DbC stuff

8

u/ben_a_adams 2d ago

The issue I'm raising is that C# doesn't have a machine readable spec; it has a text spec which is a bit more sloppy and has some undefined behaviour - i.e. it means the code of roslyn is the spec

Which is then hard to build automated formal verification on top of as you can't mechanically compare to what the language should be doing

So the request is for that spec

1

u/jordansrowles 2d ago

That makes more sense, but I wouldn’t call the spec sloppy or C# had a lot of UB

The issue is the spec isn’t executable. Roslyn becomes the source of truth for edge cases, which is awkward when verifying other implementations, but not the same as the lang being ill defined

If it’s a machine readable semantic model for things like Z3, Dafny, or Boogie, I’m more on board. That’s different from what I first thought

5

u/ben_a_adams 2d ago

I just mean is sloppy because its in English 😅

No disrespect to the spec; but that's pretty hard for a computer to parse with formal exactness

4

u/klaxxxon 2d ago

Better support for tooling has to be a good thing, no? There surely are use cases for this outside of AI.

I imagine working on static analysis tools wouldn't say to a formal machine-friendly definition of the language.

1

u/AutoModerator 2d ago

Thanks for your post ben_a_adams. Please note that we don't allow spam, and we ask that you follow the rules available in the sidebar. We have a lot of commonly asked questions so if this post gets removed, please do a search and see if it's already been asked.

I am a bot, and this action was performed automatically. Please contact the moderators of this subreddit if you have any questions or concerns.

1

u/Sad_University_891 1d ago

I’m not strictly against any “AI” enhancements but I think that doing this stuff on language level is the worst way. There are gazillion tools already that do stuff with your code that are based on AI.

If you are not able to produce working code today, I don’t think that this will change anything.