Dafny is a verification-aware programming language
> I think we can assume it won't be as efficient has hand written code
Actually, surprisingly, not necessarily the case!
If you'll refer to the discussion in https://github.com/dafny-lang/dafny/issues/601 and in https://github.com/dafny-lang/dafny/issues/547, Dafny can statically prove that certain compiler branches are not possible and will never be taken (such as out-of-bounds on index access, logical assumptions about whether a value is greater than or less than some other value, etc). This lets you code in the assumptions (__assume in C++ or unreachable_unchecked() under rust) that will allow the compiler to optimize the codegen using this information.
A static verifier for Rust, based on the Viper verification infrastructure.
You might be interested in the Prusti project, which statically checks for absence of reachable panics, overflows etc. It also allows user-defined specifications such as pre and post-conditions, loop body invariants, termination checking and so on.
Learn any GitHub repo in 59 seconds. Onboard AI learns any GitHub repo in minutes and lets you chat with it to locate functionality, understand different parts, and generate new code. Use it for free at www.getonboard.dev.
An EVM interpreter in Dafny
The Z3 Theorem Prover
I believe, Nim also has this functionality, although, it uses the Z3Prover tool with a nim frontend "DrNim" for proving.
TLC is an explicit state model checker for specifications written in TLA+. The TLA+Toolbox is an IDE for TLA+.
I wish something like Lamport's TLA+ (https://lamport.azurewebsites.net/tla/tla.html) was supported in modern language compilers - perhaps with annotations/macros and a mini formal DSL.
Executable specification language with delightful tooling (by informalsystems)
It's still in pretty early development, but you may be interested in https://github.com/informalsystems/quint
> It combines the robust theoretical basis of the Temporal Logic of Actions (TLA) with state-of-the-art static analysis and development tooling.
And it is typed ;)
Why people in Google hate Go?
4 projects | news.ycombinator.com | 3 Nov 2023
Banging Errors in Go
4 projects | news.ycombinator.com | 19 Oct 2023
Getaddrinfo() on glibc calls getenv(), oh boy
10 projects | news.ycombinator.com | 16 Oct 2023
The Top 20 Programming Languages and Their Origins
7 projects | dev.to | 24 Sep 2023
No telemetry in the Rust compiler: metrics without betraying user privacy
2 projects | news.ycombinator.com | 1 Aug 2023