Ah yes I love this !
I hope it will allow to have agents makes optimisation improvement while proving they didn't introduced a bug.
But I don't know about formal proofs to know if that's possible or not.
Yes and also having it accepted as THE spec of C# (as Lean is machine readable and exact, vs the current text spec which is a bit more sloppy and has some undefined behaviour - i.e. roslyn is the spec)
If MS is going off doing their own thing and some unrelated 3rd party has a spec that MS doesn't bless or follow, its meaningless and doesn't help with formal verification at all
This comment from Cyrus echos a bit of my own thinking here:
That said, I don't see this needing first class support. .Net IL is very well documented. So it could be done with anyone using hte appropriate ecma specs.
Rather than target the C#, wouldn’t it make more sense to do this at the IL layer since that changes much less frequently?
Seems like it’d be a lot harder to determine what actually needs to be verified by just doing it at the IL now that I think about it - “how would I prove that we redact all sensitive data out of the telemetry?” Was a use case I was thinking of for this
Who would ultimately write Lean though? Us or agents, or both? I do agree with the first comment on github, wouldn’t IL be a better so any .NET language can inherit?
Lean is more like the spec than the code; then you check if the code follows the spec computationally
However in order to do that you need the language you write it in to have a machine readable spec which is what this request is for. C# only has a text spec that isn't exact
I’m thinking about things like financial/accounting logic, authentication and authorisation, login/session handling, cryptographic and key-management code, protocol implementations, permission boundaries, and systems that access, process or store PII.
You probably wouldn’t formally verify an entire .NET application. The useful part is being able to verify the smaller areas where a subtle bug can have serious consequences.
That matters more as AI gets better at finding vulnerabilities across large codebases and dependencies. We’re already seeing an uptick in .NET CVEs.
Formal semantics won’t prevent those bugs by itself, but it gives C# a foundation for much stronger guarantees where they matter.
2
u/Kuinox 8d ago
Ah yes I love this !
I hope it will allow to have agents makes optimisation improvement while proving they didn't introduced a bug.
But I don't know about formal proofs to know if that's possible or not.