<discocaml_>
<darrenldl> others would be stramon and dirsift
chrisz has quit [Ping timeout: 246 seconds]
spip has quit [Ping timeout: 248 seconds]
bobo_ has joined #ocaml
chrisz has joined #ocaml
dstein64- has joined #ocaml
dstein64 has quit [Ping timeout: 268 seconds]
dstein64- is now known as dstein64
jao has joined #ocaml
rf has quit [Quit: Leaving]
gentauro has quit [Ping timeout: 255 seconds]
gentauro has joined #ocaml
motherfsck has quit [Ping timeout: 246 seconds]
Inst_ is now known as Inst
jao has quit [Ping timeout: 246 seconds]
trev has joined #ocaml
motherfsck has joined #ocaml
motherfsck has quit [Quit: quit]
genpaku has quit [Remote host closed the connection]
genpaku has joined #ocaml
daimrod has joined #ocaml
xgqt has quit [Ping timeout: 264 seconds]
xgqt has joined #ocaml
trillion_exabyte has quit [Ping timeout: 248 seconds]
trillion_exabyte has joined #ocaml
landonf has quit [Ping timeout: 248 seconds]
landonf_ has joined #ocaml
landonf_ is now known as landonf
mro has joined #ocaml
olle has joined #ocaml
mro has quit [Remote host closed the connection]
bgs has joined #ocaml
Tuplanolla has joined #ocaml
bartholin has joined #ocaml
Haudegen has joined #ocaml
azimut has joined #ocaml
bartholin has quit [Remote host closed the connection]
bartholin has joined #ocaml
bgs has quit [Remote host closed the connection]
amk has quit [Remote host closed the connection]
amk has joined #ocaml
mro has joined #ocaml
Serpent7776 has joined #ocaml
neiluj has quit [Ping timeout: 246 seconds]
neiluj has joined #ocaml
<neiluj>
do you think it's worth it to learn programming with dependent types? to write actual programs and corresponding proofs of correctness?
mro_ has joined #ocaml
<neiluj>
heard that the development in such languages is very slow
<neiluj>
so it is worth for "stable" programs or algorithms
mro has quit [Ping timeout: 255 seconds]
mro_ has quit [Remote host closed the connection]
mro has joined #ocaml
mro has quit [Remote host closed the connection]
<discocaml_>
<darrenldl> my uni colleague is a huge fan of idris2
<discocaml_>
<darrenldl> lean4(?) looks more user friendly than coq
<neiluj>
thanks for the input, so far I'm on the chapter on quantifiers and equality of lean tutorial, then I plan to move to Coq and maybe FStar for the extraction to C
<neiluj>
trying to mix practice and theory for now, the lean tutorial is great at this
<neiluj>
idris is nice but I prefer the ability to transpile to more performant languages
zbroyar has joined #ocaml
<reynir>
I think it's worth learning just for the "perspective". It can give inspiration to what you can do with GADT
zbroyar has quit [Ping timeout: 255 seconds]
<discocaml_>
<MasterBuilder> neiluj: Doesn't Idris have a C backend?
<neiluj>
basically besides the perspective I'm interested in proofs assistant to prove non-trivial properties about programs I write, to complement tests that can't check the program correct against all inputs
<neiluj>
and to get more help from the type checker, to write robust and memory-safe programs in C (with Fstar)
alexherbo2 has joined #ocaml
<discocaml_>
<froyo> MasterBuilder: having a C backend doesn't automatically make you fast. Idris' chez scheme backend last I heard was the fastest. Both are slow compared to your usual compiled functional language though.
<discocaml_>
<froyo> If you want a proof assistant with good support (not an experiment) and competitive performance, it is Lean4
<discocaml_>
<froyo> anecdotally I feel like I can push out proofs faster in Coq.. Lean's universes are still a bit fiddly for me when I define stuff
<discocaml_>
<masterbuilder> The only thing they said is they wanted to transpile to a "performant" language, presumably something with a mature optimizing compiler such as C
<discocaml_>
<masterbuilder> Doesn't surprise me much that the Chez backend is better, Chez is a very impressive implementation
<discocaml_>
<masterbuilder> the mapping from Idris to Scheme is considerably more direct
<neiluj>
I prefer the cleaner syntax of lean having done a tiny bit of coq, but coq is more mature
<discocaml_>
<froyo> I would be happy if a proof assistant extracts code in the average case that's in the realm of performance of OCaml and Haskell, Lean is already there with its reuse analysis powered ref-counter "Perceus".
<discocaml_>
<froyo> they're actually aiming to go even further than the average functional language though, which is commendable
<discocaml_>
<froyo> All these types and metaprogramming capabilities should be amenable to better optimization after all
<discocaml_>
<froyo> that's one of the promises of having so much static info the compiler is aware of
mro has joined #ocaml
<neiluj>
froyo: doesn't coq already extract to ocaml? performance should be fine, no?
zbroyar_ has quit [Remote host closed the connection]
mro has quit [Remote host closed the connection]
Stumpfenstiel has joined #ocaml
bobo_ has quit [Ping timeout: 246 seconds]
spip has joined #ocaml
olle has joined #ocaml
count3rmeasure has joined #ocaml
zbroyar has joined #ocaml
mro has joined #ocaml
kakadu has quit [Remote host closed the connection]
zbroyar has quit [Remote host closed the connection]
zbroyar has joined #ocaml
zbroyar has quit [Remote host closed the connection]
zbroyar has joined #ocaml
zbroyar has quit [Ping timeout: 246 seconds]
mro has quit [Remote host closed the connection]
mro has joined #ocaml
alexherbo2 has quit [Remote host closed the connection]
mro has quit [Remote host closed the connection]
jao has joined #ocaml
mro has joined #ocaml
zbroyar has joined #ocaml
zbroyar has quit [Ping timeout: 252 seconds]
<companion_cube>
neiluj: if you're fine with ocaml's perf, look at why3 or cameleer, to prove actual ocaml and not extracted code
<companion_cube>
Or even, if you want industrial strength proved code, I think Ada/SPARK is one of the strongest options
<companion_cube>
(also relies on why3)
zbroyar has joined #ocaml
<neiluj>
companion_cube: oh thanks for mentioning this projects!
<neiluj>
*these
Anarchos has joined #ocaml
xgqt has quit [Quit: WeeChat 3.6]
mro has quit [Remote host closed the connection]
xgqt has joined #ocaml
count3rmeasure has quit [Ping timeout: 268 seconds]
mro has joined #ocaml
lisq has quit []
lisq has joined #ocaml
mro has quit [Remote host closed the connection]
mro has joined #ocaml
count3rmeasure has joined #ocaml
mro has quit [Remote host closed the connection]
<olle>
Hm can ounit run single tests? Or test by name filter?
<olle>
-only-test
<olle>
Seems so
<olle>
But no text diff perhaps :d
<olle>
Btw what happened to monadic pipe operator?
<olle>
|>*
<olle>
:)
mro has joined #ocaml
mro has quit [Remote host closed the connection]
Anarchos has quit [Quit: Vision[]: i've been blurred!]
trev has quit [Remote host closed the connection]
<Fardale>
You can already define it.
<olle>
Yea?
<olle>
Kewl
<olle>
Ehm, how do I reach modules from folder lib/ from folder test/ ? With dune setup.
<olle>
lib/ast.ml specifically
<olle>
Lib.Ast - no.
<olle>
open Ast, also no
<octachron>
The name of the folder is irrelevant. What is the name of the library in the folder?
rf has joined #ocaml
<discocaml_>
<froyo> you should take that library name and add it to (libraries ...) in your test/dune
<olle>
Ehm
<olle>
Lemme try
<olle>
Yea that works, thanks!
<discocaml_>
<masterbuilder> is there no way to have explicit polymorphic annotations but also regular named parameters?
<discocaml_>
<NULL> Yes there is ?
<discocaml_>
<NULL> `let f : type a. named:int -> a t -> a` ?
<discocaml_>
<masterbuilder> but that's a label isn't it?
<discocaml_>
<NULL> What do you mean with "named parameters" then ?
<discocaml_>
<masterbuilder> like `let f x y z : ... = ...`
<discocaml_>
<NULL> You can't use that syntactic sugar, that is true
<discocaml_>
<masterbuilder> labels are fine, how do I use them in the body? didn't seem to work
<discocaml_>
<NULL> If you just need regular arguments, just write `let f : type a. a t -> a = fun x y z -> ...`
<discocaml_>
<masterbuilder> ahh, cheers
<discocaml_>
<masterbuilder> that didn't occur to me
<discocaml_>
<octachron> Also for non-recursive function, outside of polymorphic variants and objects, a locally abstract type can be enough: `let f (type a b c) (x:a) (y:b) (z:c) = ...`
<reynir>
can't you write `let f (type a) x y z : ... = ...` ?
<discocaml_>
<masterbuilder> what is the difference?
<discocaml_>
<NULL> octachron: This pretty much aligns with the cases where it's not needed for the compiler, right ?
<discocaml_>
<masterbuilder> none for non-recursive functions?
<discocaml_>
<NULL> reynir: You can, but this isn't as powerful as you might need
<discocaml_>
<octachron> @NULL for the polymorphic recursion, yes. The variants and objects are not necessary however.
<discocaml_>
<octachron> none except for the cases that I have cited.
<discocaml_>
<octachron> Basically, `type a. ...` combines both a locally abstract type binding and an universal annotation. `(type a)` is just the locally abstract type part which is sufficient for debugging.
<discocaml_>
<masterbuilder> evidently locally abstract type is not sufficient in this case
<olle>
Hum, how can I remember to run both ounit tests and inline tests?
<olle>
Can I configure dune to run both with a single command?
Anarchos has joined #ocaml
<olle>
Hey maybe chatgpt knows :D
malc has left #ocaml [ERC 5.4.1 (IRC client for GNU Emacs 29.0.50)]
Anarchos has quit [Quit: Vision[]: i've been blurred!]
<discocaml_>
<masterbuilder> companion_cube: Does Cameleer have any documentation? The Gospel docs refer the reader to the GitHub page but that does not seem to contain much information at all
<companion_cube>
Idk how far along the project is
<companion_cube>
Armael might know
<Armael>
cameleer is a bit of a WIP atm I think
<Armael>
gospel as well
rf has quit [Remote host closed the connection]
<Armael>
it is promising but it may be a bit early to use it
rf has joined #ocaml
<Armael>
cameleer is based on why3, maybe you can try to use why3 directly instead? It means you'll have to write your code in WhyML instead of OCaml (WhyML can be then translated to OCaml)
<Armael>
but then why3 should be more mature
<Armael>
(what cameleer basically does is translate OCaml code to WhyML code so that you can use why3 to verify it)
<discocaml_>
<masterbuilder> any reasons to use whyml rather than coq? I imagine whyml is considerably more straightforward
<Armael>
whyml is more geared towards practical program verification, you get much more automation with the help of solvers etc to solve verify your code
<Armael>
coq is more generic, you can use it to write verified code, but it'll be harder than using why3 for comparable tasks
<Armael>
also whyml allows you to write imperative code, while coq functions need to be pure
<discocaml_>
<masterbuilder> cool, maybe I'll have a look at whyml
<Armael>
the verification process looks different between the two: with coq you define pure functions (your code) and verify them by proving coq theorems about them
<Armael>
in why3/whyml, you write programs annotated with pre/post conditions, loop invariants and assertions interspersed with the code, and you run solvers to prove these assertions
<discocaml_>
<masterbuilder> I see
Tuplanolla has quit [Quit: Leaving.]
azimut has quit [Remote host closed the connection]
azimut has joined #ocaml
bartholin has quit [Quit: Leaving]
bartholin has joined #ocaml
Serpent7776 has quit [Ping timeout: 255 seconds]
count3rmeasure has quit [Read error: Connection reset by peer]
azimut has quit [Remote host closed the connection]
azimut has joined #ocaml
bartholin has quit [Remote host closed the connection]