Dan Drake 🦆

I'm interested in learning about formal methods and zero-knowledge proofs, particularly for their use in verifying software. I know very, very little about this, but it would be very useful if I knew more.

What are some good basic introductions?

I'm going to poke around a bit with Lean and Dafny. What else might I look at to get, at least, what you might call a "dinner party level" of understanding -- enough so that I can follow and basically participate in a conversation about those in a not-so-formal situation?

#cs #formalmethods #zkp

Mar 1 at 11:42amWeb
Show threadDan Drake 🦆Mar 1
Also, aren't dependent types related to this? I have tried to really get dependent types a few times and still don't quite understand that.
Show threadDan Drake 🦆Mar 1

One thing I do know about is that you can use these things to examine other programs or binaries and find bugs.

Would this be a reasonable little project? Write a tiny program that has a bug, like a buffer overflow, or use-after-free, or null pointer access, something like that. Then use something related to formal methods to find that?

Is that something you can do?

Show threadDima Pasechnik 🇺🇦 🇳🇱Mar 1

@ddrake try https://softwarefoundations.cis.upenn.edu/ ?

as to dinner type level dependent types - imagine you can at compile time check and set sizes of matrices used in your code (without agonising pain of C++ templates :-))

Software Foundations

Show threadDan Drake 🦆Mar 1

@dimpase for dependent types, that's roughly what I was thinking, but my memory is that every time I've looked into actually writing any code that used that kind of bound, I couldn't figure it out. For example, doing combinatorics stuff with Haskell -- I want to somehow say that the type of something is a nonnegative integer. I want regular integers, but with that extra bound guarantee. I couldn't figure it out.

But that was years ago. I should give it another go.

Show threadDima Pasechnik 🇺🇦 🇳🇱Mar 1
@ddrake Haskell has no dependent types!
You might try agda, which is close to Haskell, and does have dependent types.
Show threadRuchira S. DattaMar 2
@dimpase @ddrake Idris / Idris 2 has dependent types.
Show threadOmar AntolínMar 1
@ddrake Huh, in my mind formal methods and zero-knowledge proofs are not closely related topics, even though both are about certifying something to be true.
Show threadDan Drake 🦆Mar 1
@oantolin yep, that's the use-case for the people who do this, and I'm hoping to work with those people. Take software -- code, whatever -- can you do something with it that proves it works?
Show threadRuchira S. DattaMar 2

@ddrake The last I knew, the only book on Idris was for the previous version. However, there are both unofficial and official tutorials and documentation. E.g., see here:

https://idris-community.github.io/idris2-tutorial/Preface.html

The Idris 2 Programming Langauge - Idris 2 Tutorial