dafny VS Idris2

It's a set of asserts that are a part of the type signature. Requires are asserts on the inputs, ensures are asserts on the outputs.

Depending on your backend you either ignore them, check them all of the time, some of the time, or have SMT-solvers prove that if you uphold the first one all else must follow.

If you're interested in the last one, have a look at Dafny[0]

[0] https://dafny.org/

> The signature declares types, preconditions, postconditions, and effects. The compiler verifies the contract via SMT solver.

This reminds me of Dafny: https://dafny.org/

Actually, that would be an interesting question: how good are LLMs at writing (correct) Dafny?

In the world of software development, we spend countless hours writing tests to prevent bugs. But what if we could prove, with mathematical certainty, that our code is free of entire classes of errors? This is the promise of formal verification, and tools like Dafny are making it more accessible than ever.

Automation of Hoare logic is quite good these days. Dafny, from MS Research (https://dafny.org), is probably the most friendly formal language. Dafny has been used to verify large systems, including many components of AWS. I am hoping that LLMs make more advanced languages, such as Liquid Haskell or Agda, much easier to write. Ideally, lots of code should be autocompleted once a human provides a type signature. The advantage of formal verification is that we are sure the generated code is correct.

Modern software verification employs various approaches, each offering different trade-offs between ease of use and strength of guarantees. AWS contributes to the open source program verification tools used in the previous examples. Dafny and Kani represent two powerful approaches to program verification. Let's see how they work in practice before connecting the dots between automated reasoning and generative AI.

On that note, I discovered Dafny[1] recently, as a more accessible way to program with proofs. There's a companion book[2] that seems very accessible and down-to-earth (and, unfortunately, quite expensive). I didn't have the time to play with it yet, but it looks like it does what Ada/SPARK does (and more), but with less verbose syntax and more options for compilation targets. It seems to be actively developed, too. Personally, I had a very hard time getting into Coq, which is a proof assistant more than a programming environment - Dafny seems much more welcoming for a "working programmer" :)

[1] https://dafny.org/

[2] https://mitpress.mit.edu/9780262546232/program-proofs

https://dafny.org/ also allows proof checking and allows do write real programs with it. It has a java like syntax and is also from MS I believe

> I do think there's a bit of the Ignaz Semmelweis[1] issue at hand here, where developers want to believe in their inherent quality and refuse processes that improve safety if it goes against their worldview

I think the problem is that other variables (not only safety) must be assessed beyond the pure "better". Haskell is very good also. Very correct. Who uses that, and where? And why? Why not everyone uses https://dafny.org/ ?

it's bootstrapped off of GHC.

(i created a PR to refactor their build system to reify the bootstrap process all the way down from GHC. it basically generalized the normal build workflow of Idris2 to be able to animate the entire bootstrap chain from GHC. sadly, it was pretty much ignored, and later abandoned: https://github.com/idris-lang/Idris2/pull/1990)

Idris[1] and most of the dependent typed languages that I've looked at use de Bruijn numbers. (As does my own[2].)

The Idris implementation also has a list of names in scope as an argument to the type of a Term, which makes the compiler (also Idris) check if you're making a mistake with your de Bruijn indices. (I did not do this in mine, but I should have.)

[1]: https://github.com/idris-lang/Idris2

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

The original paper also does plain STLC first in section 2, and then adds dependent types in section 3. (And finally it adds the naturals in section 4.)

In the Idris2 github repository, Guillaume Allais goes a step further and shows a well-named version. There the types of terms and values are indexed by the list of names in the environment and the compiler checks that the manipulation of deBruin levels and indices is correct:

https://github.com/idris-lang/Idris2/blob/main/libs/papers/L...

Most of the proof assistants out there: Lean, Coq, Dafny, Isabelle, F*, Idris 2, and Agda. And the main concepts are dependent types, Homotopy Type Theory AKA HoTT, and Category Theory. Warning: HoTT and Category Theory are really dense, you're going to really need to research them.

Idris2 has a great syntax for this, see e.g. node018:

I asked because it just baffles me any time I see a dependently typed language using unary numbers. I think to myself, "are these people even educated? Do they know about number systems?" I mean, cavemen were the last group using unary number system as their mainstay, and that was during the Paleolithic. Then they have issues open like this when they discuss optimizing those damn unaries. But this shouldn't even have been a problem for anyone even remotely related to programming! It's giving a terrible impression of dependently-typed languages. Getting rid of those should be the first step of popularizing them.