<discocaml>
<tornato> But I did hear that coq and agda are mostly proof assistants
<discocaml>
<Kali> indeed
<discocaml>
<Kali> an SMT solver essentially automatically proves theorems a certain family of theorems (https://en.wikipedia.org/wiki/Satisfiability_modulo_theories), given that it can do it within a specific amount of time (you don't want it to go forever)
<discocaml>
<Kali> theorems from* a certain family of theorems
<discocaml>
<tornato> I am interested in math but more interested in proving the correctness of code if that is even possible
<discocaml>
<Kali> the smt solver proves the correctness of the code for you, when it is able to
<discocaml>
<tornato> 👀
<discocaml>
<tornato> Whoa
<discocaml>
<._null._> They rarely prove code correct, the problems they can solve are much more simple. However, the system which boils your code correctness to simple problems work in tandem with these SMTs
<discocaml>
<._null._> They rarely prove code correct *directly*, the problems they can solve are much more simple. However, the system which boils your code correctness to simple problems works in tandem with these SMTs
<discocaml>
<Kali> well, yes, but it allows you to cut out several steps that are tedious or difficult for you to prove
<discocaml>
<._null._> SMTs are rarely more intelligent than you. They can make easy work of tedious proofs however, that's for sure
<discocaml>
<._null._> SMTs are rarely more intelligent than you. They can make easy work of some tedious proofs however, that's for sure
<discocaml>
<tornato> I'll have to look into that, dependent types and SMTs
chrisz has quit [Ping timeout: 255 seconds]
chrisz has joined #ocaml
<discocaml>
<tornato> Yeah FP is a wild ride man
<discocaml>
<tornato> Gateway drug
<companion_cube>
Look into why3
<discocaml>
<tornato> That has the slowest website I've ever seen, it must be legit! Looks cool
<discocaml>
<contextfreebeer> only a little bit, I'm not the biggest fan of Haskell so that makes me automatically less interested in Idris but I think if you want to do real general-purpose dependently typed programming it is probably the best option. But in a way it's like a dependently typed Haskell with a fraction of its ecosystem, and Haskell's is already tiny, so it doesn't feel like a language you can really jump into, but if you're dedicated it could be a g
<discocaml>
<contextfreebeer> Don't bother with dependently typed programming in Coq, you really need to be an expert in Coq and understand how it works to have any success with that, it's like the assembly of dependently typed programming, overall very tedious and difficult to use, for modeling and proofs, and extracting non-dependent programs it is great though
<discocaml>
<peuk> Why3 is good for writing programs and proving them. Use Why3.
<discocaml>
<contextfreebeer> I think the best way to get into that kind of programming is probably through "inline" specifications that get translated along with your code and sent to SMT solvers to verify automatically, as mentioned SMT solvers can't prove everything automatically (because it is undecidable) but as a beginner you can probably only prove relatively "trivial" stuff anyway. I think F* is great because it supports (boolean) refinement types which fee