00:00 <discocaml> <tornato> But I did hear that coq and agda are mostly proof assistants

00:00 <discocaml> <Kali> indeed

00:02 <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)

00:02 <discocaml> <Kali> theorems from* a certain family of theorems

00:02 <discocaml> <tornato> I am interested in math but more interested in proving the correctness of code if that is even possible

00:04 <discocaml> <Kali> the smt solver proves the correctness of the code for you, when it is able to

00:04 <discocaml> <tornato> 👀

00:04 <discocaml> <tornato> Whoa

00:05 <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

00:05 <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

00:06 <discocaml> <Kali> well, yes, but it allows you to cut out several steps that are tedious or difficult for you to prove

00:07 <discocaml> <._null._> SMTs are rarely more intelligent than you. They can make easy work of tedious proofs however, that's for sure

00:07 <discocaml> <._null._> SMTs are rarely more intelligent than you. They can make easy work of some tedious proofs however, that's for sure

00:08 <discocaml> <tornato> I'll have to look into that, dependent types and SMTs

00:11 <discocaml> <tornato> Yeah FP is a wild ride man

00:12 <discocaml> <tornato> Gateway drug

00:14 <companion_cube> Look into why3

00:20 <discocaml> <tornato> That has the slowest website I've ever seen, it must be legit! Looks cool

00:29 <discocaml> <yawaramin> and Ada SPARK 🙂

00:31 <companion_cube> Which builds on why3, yeah

00:31 <companion_cube> Hu? Why3's website, slow?

00:36 <discocaml> <tornato> It must've been a fluke

00:36 <discocaml> <tornato> Seems fine now (or maybe it's cached)

03:02 <discocaml> <gunpowderguy> Does ocaml support dependent types

03:02 <discocaml> <gunpowderguy> Does ocaml support dependent types?

03:04 <discocaml> <Kali> only a limited form through GADTs, but in general, no

08:46 <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

08:47 <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

09:08 <discocaml> <peuk> Why3 is good for writing programs and proving them. Use Why3.

09:11 <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

14:14 <adrien> I'm using (!=) and this constraints the types of the two operands to be equal which causes me issues down the road; I solved that by using Obj.magic but I'd prefer to avoid it

14:14 <adrien> I'm a bit surprised that (!=) is 'a -> 'a -> bool rather than 'a -> 'b -> bool, is there a specific reason for that?

14:15 <discocaml> <._null._> What would the result of `0 = []` be?

14:16 <discocaml> <._null._> Oh, wait, you're specifically talking about physical equality

14:17 <adrien> yes, but wouldn't 0 and [] compare equal using physical equality? :P

14:17 <discocaml> <._null._> Still, `0 == []` looks confusing

14:18 <discocaml> <._null._> What's the purpose of comparing elements of different types?

14:18 <adrien> also, more context: I'm using lambdasoup and it has "element node" and "general node", and I'm iterating over a list of general nodes, among which one element node I want to skip

14:19 <adrien> and I have a way around: move/rename everything and then change how I handle that specific node

14:20 <adrien> my concern is that the performance is currently good but it has been yoyo'ing for a while (from 3 seconds to 240 seconds)

14:22 <octachron> You can define "type any = Any: 'a -> any [@@unboxed]" and "let (=/=) x y = (Any x) != (Any y)"

14:24 <octachron> I forgot that you need to specialize the `'a` in the `Any` definition to make it unboxable

14:25 <octachron> But `type any_node = Any: 'a node -> any_node [@@unboxed]` should be safer anyway.

14:37 <adrien> the compiler complains that there could be float values and non-float values and the type therefore cannot be unboxed

14:39 <adrien> tried a few things but only found dead ends

14:57 <octachron> Ah, yes if the type is abstract, it is not possible to unbox it.

14:59 <adrien> I think I'll try the other approach and move/rename nodes a bit later; I still have a lot to do and the shitty structure of my input is the biggest constraint at the moment

15:00 <adrien> (the input is a pure-html file than can almost crash all current browsers; there's also a companion input that regularly reliably crashes all browsers :P )

15:31 <companion_cube> can't wait for a tag that says "this opaque type is not immediate"

15:31 <companion_cube> I've had to expose definitions because of that :/

15:35 <olle> Which types can be unboxed now?

15:36 <companion_cube> `type foo = Foo of <some non-immediate type>`

15:39 <olle> companion_cube: link that describes non-immediate?

15:46 <discocaml> <hockletock> ints, bools, chars, probably something I'm forgetting, types that are transparently aliases of these

15:47 <discocaml> <hockletock> err, those are immediate

15:48 <discocaml> <._null._> All constant constructors are immediates. Types can have both immediate and non-immediate values

15:48 <olle> https://www.janestreet.com/tech-talks/unboxed-types-for-ocaml/

23:46 <discocaml> <gunpowderguy> What languages do you feel idris2 Is sorely lacking that prevent it from being a language you can just jump into?

23:58 <discocaml> <contextfreebeer> libraries*?

23:58 <discocaml> <gunpowderguy> Sorry,libraries

23:59 <discocaml> <gunpowderguy> What libraries do you feel idris2 Is sorely lacking that prevent it from being a language you can just jump into?

23:59 <discocaml> <contextfreebeer> Well, I'm not deep in the Idris community, or even at all, so I couldn't tell you exactly, it's just a feeling I got when I tried it out, no doubt it has much improved since then