Make formal verification and provably correct software practical and mainstream

• magmide

  22 803 6.6 Coq

  A dependently-typed proof language intended to make provably correct bare metal code possible for working software engineers.

  

I really want to like this, but it really comes across as more of a wishful thinking project without a lot of experience or intuition about how to solve the very real problems that formal methods run into in this domain. Like, the design goals literally include "verify any program" [1], which is almost certainly impossible.

Important questions like how you implement the design pillars without running smack into the issue of decidability seem entirely ignored. They have a whole section on how "this idea exists in an incentive no man's land" without seemingly being aware of the rich history of formal methods in low level programming, from Ada through Java through formal C through Rust itself. The common issues these encountered like decidability, holes in the formal model (which contributed to the downfall of the Java sandbox as a security boundary), and the combinatorial explosion inherent in verification tools are all huge looming questions that should at least be mentioned.

Maybe I'm being overly critical here, but it all makes me wonder whether the project is even possible.

[1] https://github.com/magmide/magmide/blob/main/posts/design-of...

• flexbugs

  9 13,647 0.0

  Discontinued A community-curated list of flexbox issues and cross-browser workarounds for them.

For functional stuff, sure, but I don't think this is achievable within the UI domain. CSS rules have implementation details that change how you write it, for example there's a documented set of issues in flex implementations maintained here: https://github.com/philipwalton/flexbugs

It might be practical and possible to become mainstream for some domains, but it's doubtful for others.

• InfluxDB

  www.influxdata.com sponsored

  Power Real-Time Data Analytics at Scale. Get real-time insights from all types of time series data with InfluxDB. Ingest, query, and analyze billions of data points in real-time with unbounded cardinality.

  

• dafny

  31 2,665 9.7 C#

  Dafny is a verification-aware programming language

  

It is still alive, it has just moved to github! It is a big language and it can prove useful programs. Apparently, part of the Ethereum 2 specification was verified using it. https://github.com/dafny-lang/dafny

• z3

  28 9,708 9.8 C++

  The Z3 Theorem Prover

  

• .NET Runtime

  607 14,091 10.0 C#

  .NET is a cross-platform runtime for cloud, mobile, desktop, and IoT apps.

  

• csharplang

  262 10,868 9.6 C#

  The official repo for the design of the C# programming language

  

Suggest a related project