Lean4 helped Terence Tao discover a small bug in his recent paper

1. z3

   1 33 11,165 9.9 C++

   The Z3 Theorem Prover

   

   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

2. Stream

   getstream.io featured

   Stream - Scalable APIs for Chat, Feeds, Moderation, & Video. Stream helps developers build engaging apps that scale to millions with performant and flexible Chat, Feeds, Moderation, and Video APIs and SDKs powered by a global edge network and enterprise-grade infrastructure.

   

3. CodeContracts

   2 3 850 0.0 C#

   Discontinued Source code for the CodeContracts tools for .NET

   

   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

4. dafny

   3 38 3,112 9.5 C#

   Dafny is a verification-aware programming language

   

   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

5. cedar-spec

   4 3 118 9.3 Lean

   Definitional implementation of Cedar language and utilities for DRT

   

   Note that the Z3 SMT solver was written by Leonardo de Moura, who also is the lead dev of Lean 4. Not a coincidence (-;

   Lean 4 seems to be used in production at AWS: https://github.com/cedar-policy/cedar-spec/pull/138

6. FStar

   5 48 2,864 9.9 F*

   A Proof-oriented Programming Language

   

7. Idris2

   6 40 2,685 8.9 Idris

   A purely functional programming language with first class types

   

   Have you looked into Idris2 at all. While looking into these theorum provers, it always felt like they had an impedance mismatch with normal programming.

   Idris2 portends to a general purpose language that also has a more advanced type system for the theorum proving.

   https://github.com/idris-lang/Idris2

8. symmetric_project

   7 1 87 9.1 Lean

   

   You can even follow his progress on GitHub here:

   https://github.com/teorth/symmetric_project/

9. InfluxDB

   www.influxdata.com featured

   InfluxDB – Built for High-Performance Time Series Workloads. InfluxDB 3 OSS is now GA. Transform, enrich, and act on time series data directly in the database. Automate critical tasks and eliminate the need to move data externally. Download now.

   

10. lean4

    8 62 5,903 10.0 Lean

    Lean 4 programming language and theorem prover

    

    Yeah, I believe they said intend for it to be used as a general purpose programming language. I used it to complete Advent of Code last year.

    There are some really interesting features for general purpose programming in there. For example: you can code updates to arrays in a functional style (change a value, get a new array back), but if the refcount is 1, it updates in place. This works for inductive types and structures, too. So I was able to efficiently use C-style arrays (O(1) update/lookup) while writing functional code. (paper: https://arxiv.org/abs/1908.05647 )

    Another interesting feature is that the "do" blocks include mutable variables and for loops (with continue / break / return), that gets compiled down to monad operations. (paper: https://dl.acm.org/doi/10.1145/3547640 )

    And I'm impressed that you can add to the syntax of the language, in the same way that the language is implemented, and then use that syntax in the next line of code. (paper: https://lmcs.episciences.org/9362/pdf ). There is an example in the source repository that adds and then uses a JSX-like syntax. (https://github.com/leanprover/lean4/blob/master/tests/playgr... )

11. CoqGym

    9 2 405 3.6 Coq

    A Learning Environment for Theorem Proving with the Coq proof assistant

    

12. idris2-pack-db

    10 1 26 9.6

    

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

Suggest a related project