CodeContracts
symmetric_project | CodeContracts | |
---|---|---|
1 | 3 | |
78 | 850 | |
- | - | |
9.1 | 0.0 | |
6 months ago | over 5 years ago | |
Lean | C# | |
- | GNU General Public License v3.0 or later |
Stars - the number of stars that a project has on GitHub. Growth - month over month growth in stars.
Activity is a relative number indicating how actively a project is being developed. Recent commits have higher weight than older ones.
For example, an activity of 9.0 indicates that a project is amongst the top 10% of the most actively developed projects that we are tracking.
symmetric_project
-
Lean4 helped Terence Tao discover a small bug in his recent paper
You can even follow his progress on GitHub here:
https://github.com/teorth/symmetric_project/
CodeContracts
-
Remembering Bell Labs as legendary idea factory prepares to leave N.J. home
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).
-
Lean4 helped Terence Tao discover a small bug in his recent paper
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
- #if WINDOWS : use GetAsncyKeyState
What are some alternatives?
cedar-spec - Definitional implementation of Cedar language and utilities for DRT
Git Diff Margin - Git Diff Margin displays live Git changes of the currently edited file on Visual Studio margin and scroll bar. Supports Visual Studio 2012 through Visual Studio 2022
dafny - Dafny is a verification-aware programming language
OzCode - Demos that show the power of OzCode
Idris2 - A purely functional programming language with first class types
Refactoring Essentials - Refactoring Essentials for Visual Studio
idris2-pack-db
Side-Waffle - A collection of Item- and Project Templates for Visual Studio
CoqGym - A Learning Environment for Theorem Proving with the Coq proof assistant
VSColorOutput - Color highlighting to Visual Studio's Build and Debug Output Windows
FStar - A Proof-oriented Programming Language
Web Essentials - Visual Studio extension