CodeContracts VS idris2-pack-db

compile-time part of system could support any assertion represented as a pure-function - think of it as C#'s take on Ada's assertions, improved tenfold, and it even shipped for a now-unsupported older version of C# and .NET: https://learn.microsoft.com/en-us/dotnet/framework/debug-tra...

...and it was axed in .NET Core back in 2016 and hasn't been seen since: https://github.com/microsoft/CodeContracts/issues/409

Had Microsoft put more backing behind it, then C# could present itself as a language to supplant Ada in safety-critical applications, and replace C/C++ in other applications.

I have hope the feature will come back one-day - there are whole slews of bugs that can be eliminated (such as when passing EF entity types around with unintentionally null member-properties).

Code correctness is a lost art. I requirement to think in abstractions is what scares a lot of devs to avoid it. The higher abstraction language (formal specs) focus on a dedicated language to describe code, whereas lower abstractions (code contracts) basically replace validation logic with a better model.

C# once had Code Contracts[1]; a simple yet powerful way to make formal specifications. The contracts was checked at compile time using the Z3 SMT solver[2]. It was unfortunately deprecated after a few years[3] and once removed from the .NET Runtime it was declared dead.

The closest thing C# now have is probably Dafny[4] while the C# dev guys still try to figure out how to implement it directly in the language[5].

[1] https://www.microsoft.com/en-us/research/project/code-contra...

[2] https://github.com/Z3Prover/z3

[3] https://github.com/microsoft/CodeContracts

[4] https://github.com/dafny-lang/dafny

[5] https://github.com/dotnet/csharplang/issues/105

There's a list of packages here: https://github.com/stefan-hoeck/idris2-pack-db/blob/main/STA...