CodeContracts
CoqGym
CodeContracts | CoqGym | |
---|---|---|
3 | 2 | |
850 | 370 | |
- | 0.8% | |
0.0 | 3.6 | |
over 5 years ago | 10 months ago | |
C# | Coq | |
GNU General Public License v3.0 or later | GNU Lesser General Public License v3.0 only |
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.
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
CoqGym
- Lean4 helped Terence Tao discover a small bug in his recent paper
-
Discussion Thread
This has been an active area of research for a few years. See for example https://arxiv.org/abs/1905.09381. It's still immature as a field, and most results are essentially "we got basic stuff down but it hasn't gotten powerful enough to prove anything truly challenging" but it definitely exists and is being developed.
What are some alternatives?
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
lean - Lean Theorem Prover
OzCode - Demos that show the power of OzCode
coq - Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.
Refactoring Essentials - Refactoring Essentials for Visual Studio
trepplein - Lean type-checker written in Scala.
Side-Waffle - A collection of Item- and Project Templates for Visual Studio
mathlib - Lean 3's obsolete mathematical components library: please use mathlib4
VSColorOutput - Color highlighting to Visual Studio's Build and Debug Output Windows
lean-chat
Web Essentials - Visual Studio extension
symmetric_project