Leonidas changed the topic of #ocaml to: Discussion about the OCaml programming language | http://www.ocaml.org | OCaml 5.1.1 released: https://ocaml.org/releases/5.1.1 | Try OCaml in your browser: https://try.ocamlpro.com | Public channel logs at https://libera.irclog.whitequark.org/ocaml/
<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> <yawaramin> and Ada SPARK 🙂
oriba has quit [Quit: https://quassel-irc.org - Chat comfortably. Anywhere.]
<companion_cube> Which builds on why3, yeah
<companion_cube> Hu? Why3's website, slow?
<discocaml> <tornato> It must've been a fluke
<discocaml> <tornato> Seems fine now (or maybe it's cached)
Tuplanolla has quit [Quit: Leaving.]
motherfsck has joined #ocaml
Square2 has quit [Ping timeout: 268 seconds]
waleee has quit [Ping timeout: 260 seconds]
<discocaml> <gunpowderguy> Does ocaml support dependent types
<discocaml> <gunpowderguy> Does ocaml support dependent types?
<discocaml> <Kali> only a limited form through GADTs, but in general, no
gentauro has quit [Ping timeout: 252 seconds]
gentauro has joined #ocaml
mbuf has joined #ocaml
jabuxas has quit [Ping timeout: 260 seconds]
ansiwen has quit [Quit: ZNC 1.7.1 - https://znc.in]
ansiwen has joined #ocaml
zanetti has joined #ocaml
zanetti has quit [Quit: zanetti]
bartholin has joined #ocaml
Serpent7776 has joined #ocaml
Serpent7776 has quit [Ping timeout: 268 seconds]
bartholin has quit [Quit: Leaving]
olle has joined #ocaml
dnh has joined #ocaml
Serpent7776 has joined #ocaml
<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
waleee has joined #ocaml