csakatok_ has quit [Remote host closed the connection]
csakatoku has joined #ocaml
csakatoku has quit [Ping timeout: 240 seconds]
ulfdoz has quit [Ping timeout: 256 seconds]
osa1 has quit [Quit: Konversation terminated!]
zRecursive has joined #ocaml
f[[x]] has joined #ocaml
f[x] has quit [Ping timeout: 240 seconds]
mcclurmc has quit [Quit: Leaving.]
ulfdoz has joined #ocaml
skchrko has quit [Quit: Leaving]
pzv has quit [Quit: leaving]
zRecursive has left #ocaml []
zpe has joined #ocaml
skchrko has joined #ocaml
mcclurmc has joined #ocaml
ulfdoz has quit [Ping timeout: 276 seconds]
Drup has joined #ocaml
q66 has joined #ocaml
introom has quit [Remote host closed the connection]
osa1 has joined #ocaml
introom has joined #ocaml
jpdeplaix has quit [Ping timeout: 264 seconds]
ollehar has joined #ocaml
dsheets has joined #ocaml
Drup has quit [Ping timeout: 256 seconds]
mye has joined #ocaml
beckerb has joined #ocaml
f[[x]] has quit [Ping timeout: 256 seconds]
introom has quit [Remote host closed the connection]
mcclurmc has quit [Excess Flood]
mcclurmc has joined #ocaml
Drup has joined #ocaml
zpe has quit [Remote host closed the connection]
yezariaely has quit [Read error: Operation timed out]
eikke has quit [Ping timeout: 268 seconds]
yezariaely has joined #ocaml
zpe has joined #ocaml
osa1 has quit [Quit: Konversation terminated!]
osa1 has joined #ocaml
zpe has quit [Ping timeout: 256 seconds]
Zeev has quit [Read error: Connection reset by peer]
Zeev has joined #ocaml
Zeev has quit [Read error: Connection reset by peer]
_andre has joined #ocaml
zpe has joined #ocaml
Zeev has joined #ocaml
Zeev has left #ocaml []
zpe has quit [Ping timeout: 260 seconds]
tane has joined #ocaml
csakatoku has joined #ocaml
osa1 has quit [Quit: Konversation terminated!]
osa1 has joined #ocaml
yezariaely has quit [Ping timeout: 268 seconds]
smondet has joined #ocaml
yezariaely has joined #ocaml
f[[x]] has joined #ocaml
zpe has joined #ocaml
gautamc has quit [Read error: Connection reset by peer]
gautamc has joined #ocaml
zpe has quit [Ping timeout: 268 seconds]
osa1 has quit [Quit: Konversation terminated!]
tobiasBora has joined #ocaml
introom has joined #ocaml
tobiasBora has quit [Quit: Konversation terminated!]
zpe has joined #ocaml
tobiasBora has joined #ocaml
zpe has quit [Ping timeout: 240 seconds]
mort___ has joined #ocaml
palomer has joined #ocaml
Simn has quit [Ping timeout: 276 seconds]
Simn has joined #ocaml
introom has quit [Remote host closed the connection]
introom has joined #ocaml
palomer has quit [Ping timeout: 264 seconds]
zpe has joined #ocaml
Simn has quit [Ping timeout: 276 seconds]
osa1 has joined #ocaml
ollehar has quit [Ping timeout: 240 seconds]
tobiasBora has quit [Remote host closed the connection]
zpe has quit [Ping timeout: 248 seconds]
osa1 has quit [Ping timeout: 256 seconds]
palomer has joined #ocaml
shinnya has joined #ocaml
Simn has joined #ocaml
zpe has joined #ocaml
bkpt has joined #ocaml
mort___ has quit [Quit: Leaving.]
introom has quit [Remote host closed the connection]
yezariaely has quit [Ping timeout: 248 seconds]
zpe has quit [Ping timeout: 264 seconds]
palomer has quit [Ping timeout: 268 seconds]
mika1 has quit [Quit: Leaving.]
cago has left #ocaml []
skchrko has quit [Quit: Leaving]
NaCl_ is now known as NaCl
djcoin has quit [Quit: WeeChat 0.4.0]
zpe has joined #ocaml
fgas has joined #ocaml
fgas has quit [Client Quit]
_habnabit has quit [Remote host closed the connection]
_habnabit has joined #ocaml
beckerb has quit [Ping timeout: 245 seconds]
palomer has joined #ocaml
Neros has joined #ocaml
jpdeplaix has joined #ocaml
f[[x]] has quit [Remote host closed the connection]
ulfdoz has joined #ocaml
ygrek has joined #ocaml
darkf has quit [Quit: Leaving]
csakatoku has quit [Remote host closed the connection]
ttamttam has quit [Quit: ttamttam]
Anarchos has joined #ocaml
ulfdoz has quit [Ping timeout: 256 seconds]
Arsenik has joined #ocaml
<Anarchos>
Say f() is a C function using CAMLparam macros and doing callbacks to ocaml. Is it mandatory to call caml_acquire_runtime_system before CAMLparam macros if there are multiple C threads calling this function f() at the same time ?
<mrvn>
don't drop the lock in the first place
wmeyer` has joined #ocaml
<mrvn>
But if you don't have it then you haave to acquire it
<wmeyer`>
hi
wmeyer` is now known as wmeyer
<pippijn>
Anarchos: whenever you call ocaml code, you must acquire the lock
csakatoku has joined #ocaml
<wmeyer>
hi pippijn
<wmeyer>
it's so sunny here
<pippijn>
hi
<pippijn>
same here
<Anarchos>
pippijn yes but CAMLlocal, is it thread safe if i used caml_c_thread_register previously ?
<Anarchos>
my experience says not...
<Drup>
not same here, and I'm quite happy not to feel like in an oven again. ;)
<pippijn>
Anarchos: what about CAMLlocal?
<wmeyer>
Drup: it has certain advantages! (especially on the beach; under umbrella; with a coctail; and laptop - never tried but may do so) here was quite hot for past few days, now it's chiling, but the sun is quite remarkable
<pippijn>
whenever you do something that involves the runtime (such as allocating memory, serialisation, ...) you need to acquire the lock
<mrvn>
I would acquire the lock
<mrvn>
and carefull with your OCAMLParams, that won't do without lock
* wmeyer
eating French camembert mhmmm
<pippijn>
CAMLparam modifies global data, so you need a lock
<mrvn>
eating fried French^W^WFrench fries.
<wmeyer>
mrvn: with vinegar?
<mrvn>
read&white
<mrvn>
no mustard, no vinegar. bah
<wmeyer>
if it's not vinegar then it's not french (myself never risked adding vinegar to fries))
<pippijn>
vinegar..
<pippijn>
that's british :\
<Anarchos>
pippijn it is not mentionend in the official doc ??
<wmeyer>
yeah, it came from France!
<pippijn>
vinegar and ink
<wmeyer>
but it's common
<wmeyer>
but i don't do this
<wmeyer>
maybe when i will have a british citizenship i will start
<pippijn>
I wouldn't
<wmeyer>
y
<Drup>
wmeyer: vinegar in fries ? O_o I'm not sure we're talking about the same france here
<wmeyer>
Drup: I thought you add vinegar to everything
<Anarchos>
pippijn the manual just says to call caml_c_thread_register, not to acquire the runtime lock before CAMLparam macros
csakatoku has quit [Ping timeout: 240 seconds]
<pippijn>
The OCaml run-time system is not reentrant: at any time, at most one thread can be executing OCaml code or C code that uses the OCaml run-time system. Technically, this is enforced by a “master lock” that any thread must hold while executing such code.
<wmeyer>
Drup: sorry to accuses you for such perversion
<pippijn>
I have to install ocaml in this every time I build
manizzle has joined #ocaml
<pippijn>
if I have to build ocaml and all dependencies from scratch each time, it will take too much time
<wmeyer>
rks`_: the problem with gerd packages, is that he uses very cathedral approach to development. Otherwise they are all very high quality.
<rks`_>
wmeyer: I was just teasing
<wmeyer>
haha I know
<rks`_>
no need to get into that here
<wmeyer>
but i am honest
<rks`_>
I know you are :)
Anarchos has quit [Quit: Vision[0.9.7-H-130604]: i've been blurred!]
<pippijn>
mrvn: should I first make a bug that asks for parmap to be put into debian?
<mrvn>
pippijn: filing a RFP and including the url for the ppa is probably simplest
<wmeyer>
I have to look at ocamlbuild, this week, but so far me git svn fails at the moment at ARM device. But I do have a plenty of stuff to do too apart from that :-)
ontologiae has quit [Read error: Operation timed out]
<dsheets>
the ocamlbuild invocation is $ ocamlbuild -use-ocamlfind -tag thread -lflags -dllib,-lsodium -pkgs ctypes.foreign,bigarray lib/sodium.cma
<mrvn>
shouldn't there be a -pkgs thread?
<wmeyer>
I thnk you have to use, use_thread
<wmeyer>
rks`_: thanks :-)
skchrko has joined #ocaml
<dsheets>
mrvn, -pkgs threads? it is the same... threads is required by this version of ctypes
<rks`_>
wmeyer: btw, I don't remember if I answered you yesterday so : "oh great, thanks!" (about bin_annot)
<wmeyer>
rks`_: haha :-)
<pippijn>
mrvn: reportbug asks what package I want to report a bug about
<wmeyer>
dsheets: actually "thread" is correct
<pippijn>
should I say "other"?
<dsheets>
wmeyer, -tag thread, you mean? why is it erroring?
<pippijn>
ah, wnpp
<wmeyer>
rks`_: it takes a bit of time though to know if this feature exists in ocamlbuild, maybe I should really think about improving the documentation
<wmeyer>
because it links
<wmeyer>
only
hcarty has quit [Ping timeout: 240 seconds]
<wmeyer>
try to clean up the object files dsheets
<wmeyer>
it's a linker problem, and you have to compile with -thread too.
<dsheets>
yes... why is it generating a non-thread link command when it has the thread tag for this target?
<wmeyer>
the best would be if ocamlbuild checked it, if the command is the same, and having a flag to not force rebuilding whole project if the command line chnged
<dsheets>
i am using ocamlbuild for each component to be built without intermediate cleaning. is that so bad?
<wmeyer>
I thought you just added it
<mrvn>
wmeyer: overkill imho. how often do you change that line?
<wmeyer>
so you have build something, and then linked with -thread
<wmeyer>
well, you have to use -tags "true: thread"
<gasche>
19:49 < wmeyer> rks`_: it takes a bit of time though to know if this feature exists in ocamlbuild, maybe I should really think about improving the documentation
<gasche>
you mean that rks`_ should have done "ocamlbuild -documentation | grep annot"
<mrvn>
In oasis you simply add "BuildDepends: thread"
<wmeyer>
gasche: it's useful bot not documented!
manizzle has quit [Ping timeout: 264 seconds]
<wmeyer>
oh maybe it is
<Drup>
gasche: bin-annot is not (yet) in the stable ocamlbuild
<gasche>
I have written a blog post about this
<gasche>
Drup: fair point
<pippijn>
mrvn: it should be an ITP, right?
gautamc has quit [Read error: Connection reset by peer]
<wmeyer>
gasche: it isn't? I thought it was added last year
<dsheets>
i started with oasis but it seemed overkill and annoying to get it to do the $(CC) -shared -o $@ -lsodium bit
<mrvn>
pippijn: No. That is when you want to maintain it.
<dsheets>
i need it because the ctypes dependency on this branch uses it? i'm not entirely clear on why -thread is special vs another kind of interface/link?
<pippijn>
oh, there is an X-Debbugs-Cc
manizzle has joined #ocaml
<wmeyer>
so I'd need to look at the runtime system to know what -thread exactly does
clog has joined #ocaml
bitbckt has quit [Remote host closed the connection]
zpe has joined #ocaml
bitbckt has joined #ocaml
Drup has joined #ocaml
ggole has quit []
zpe has quit [Ping timeout: 240 seconds]
tane has joined #ocaml
gautamc has quit [Ping timeout: 264 seconds]
dsheets has quit [*.net *.split]
q66 has quit [*.net *.split]
compnaion_cbue has quit [*.net *.split]
bholst_ has quit [*.net *.split]
mal``` has quit [*.net *.split]
ipoulet_ has quit [*.net *.split]
letoh has quit [*.net *.split]
fayden has quit [*.net *.split]
jlouis has quit [*.net *.split]
rgrinberg has quit [*.net *.split]
hnrgrgr has quit [*.net *.split]
othiym23 has quit [*.net *.split]
Sim_n has joined #ocaml
dsheets has joined #ocaml
q66 has joined #ocaml
compnaion_cbue has joined #ocaml
bholst_ has joined #ocaml
mal``` has joined #ocaml
ipoulet_ has joined #ocaml
letoh has joined #ocaml
fayden has joined #ocaml
jlouis has joined #ocaml
rgrinberg has joined #ocaml
hnrgrgr has joined #ocaml
othiym23 has joined #ocaml
yacks has quit [Ping timeout: 246 seconds]
madroach has quit [*.net *.split]
gbluma has quit [*.net *.split]
Qrntz has quit [*.net *.split]
vbmithr has quit [*.net *.split]
Jenza has quit [*.net *.split]
troydm has quit [*.net *.split]
josch_ has quit [*.net *.split]
lenstr has quit [*.net *.split]
adrien_oww has quit [*.net *.split]
cow-orker has quit [*.net *.split]
emias has quit [*.net *.split]
dsheets has quit [*.net *.split]
q66 has quit [*.net *.split]
compnaion_cbue has quit [*.net *.split]
bholst_ has quit [*.net *.split]
mal``` has quit [*.net *.split]
ipoulet_ has quit [*.net *.split]
letoh has quit [*.net *.split]
fayden has quit [*.net *.split]
jlouis has quit [*.net *.split]
rgrinberg has quit [*.net *.split]
hnrgrgr has quit [*.net *.split]
othiym23 has quit [*.net *.split]
mye has quit [*.net *.split]
rednovae_ has quit [*.net *.split]
metasyntax has quit [*.net *.split]
wormphlegm has quit [*.net *.split]
osnr has quit [*.net *.split]
rks`_ has quit [*.net *.split]
Nahra_ has quit [*.net *.split]
j0sh has quit [*.net *.split]
djcoin has quit [*.net *.split]
jpdeplaix has quit [*.net *.split]
dtg has quit [*.net *.split]
pango has quit [*.net *.split]
ttm has quit [*.net *.split]
orbitz has quit [*.net *.split]
mathieui has quit [*.net *.split]
cdidd has quit [*.net *.split]
ccasin has quit [*.net *.split]
willb1 has quit [*.net *.split]
Sim_n has quit [*.net *.split]
Drup has quit [*.net *.split]
manizzle has quit [*.net *.split]
Arsenik has quit [*.net *.split]
Simn has quit [*.net *.split]
tchell has quit [*.net *.split]
NaCl has quit [*.net *.split]
gnuvince has quit [*.net *.split]
_andre has quit [*.net *.split]
bkpt has quit [*.net *.split]
contempt has quit [*.net *.split]
xaimus has quit [*.net *.split]
so has quit [*.net *.split]
tane has quit [*.net *.split]
pkrnj has quit [*.net *.split]
skchrko has quit [*.net *.split]
_habnabit has quit [*.net *.split]
thomasga has quit [*.net *.split]
asmanur has quit [*.net *.split]
hyperboreean has quit [*.net *.split]
logicgeezer has quit [*.net *.split]
balouis has quit [*.net *.split]
MarcWeber has quit [*.net *.split]
whitequark has quit [*.net *.split]
flux has quit [*.net *.split]
smondet has quit [*.net *.split]
pr has quit [*.net *.split]
Asmadeus has quit [*.net *.split]
tlockney has quit [*.net *.split]
chris2 has quit [*.net *.split]
bernardofpc has quit [*.net *.split]
ia0 has quit [*.net *.split]
Cypi has quit [*.net *.split]
quelu_ has quit [*.net *.split]
ski has quit [*.net *.split]
rossberg__ has quit [*.net *.split]
demonimin has quit [*.net *.split]
vpm has quit [*.net *.split]
adrien has quit [*.net *.split]
ohama has quit [*.net *.split]
xenocons has quit [*.net *.split]
davekong has quit [*.net *.split]
ggherdov has quit [*.net *.split]
Ptival has quit [*.net *.split]
Leonidas has quit [*.net *.split]
lopex has quit [*.net *.split]
dezzy has quit [*.net *.split]
lusory has quit [*.net *.split]
alexey has quit [*.net *.split]
Armael has quit [*.net *.split]
pippijn has quit [*.net *.split]
aggelos__ has quit [*.net *.split]
PM has quit [*.net *.split]
zzz_ has quit [*.net *.split]
tianon has quit [*.net *.split]
iZsh has quit [*.net *.split]
talzeus_ has quit [*.net *.split]
olasd has quit [*.net *.split]
gereedy has quit [*.net *.split]
jave has quit [*.net *.split]
Khady has quit [*.net *.split]
stomp has quit [*.net *.split]
palomer has quit [*.net *.split]
wmeyer has quit [*.net *.split]
rwmjones has quit [*.net *.split]
mrvn has quit [*.net *.split]
cthuluh has quit [*.net *.split]
def-lkb_ has quit [*.net *.split]
tizoc has quit [*.net *.split]
bobry has quit [*.net *.split]
bacam has quit [*.net *.split]
deavid has quit [*.net *.split]
wagle has quit [*.net *.split]
cross has quit [*.net *.split]
samebchase has quit [*.net *.split]
nicoo has quit [*.net *.split]
SuperNoeMan has quit [*.net *.split]
patronus has quit [*.net *.split]
weie has quit [*.net *.split]
sgnb has quit [*.net *.split]
caligula__ has quit [*.net *.split]
fds_ has quit [*.net *.split]
thelema has quit [*.net *.split]
gasche has quit [*.net *.split]
bitbckt has quit [*.net *.split]
yroeht1 has quit [*.net *.split]
buddyholly has quit [*.net *.split]
maxibolt has quit [*.net *.split]
levi has quit [*.net *.split]
mehdid has quit [*.net *.split]
rixed has quit [*.net *.split]
ivan\ has quit [*.net *.split]
mfp has quit [*.net *.split]
noplamodo has quit [*.net *.split]
othiym23 has joined #ocaml
hnrgrgr has joined #ocaml
rgrinberg has joined #ocaml
jlouis has joined #ocaml
fayden has joined #ocaml
letoh has joined #ocaml
ipoulet_ has joined #ocaml
mal``` has joined #ocaml
bholst_ has joined #ocaml
compnaion_cbue has joined #ocaml
q66 has joined #ocaml
dsheets has joined #ocaml
Sim_n has joined #ocaml
tane has joined #ocaml
Drup has joined #ocaml
bitbckt has joined #ocaml
djcoin has joined #ocaml
palomer has joined #ocaml
pkrnj has joined #ocaml
manizzle has joined #ocaml
skchrko has joined #ocaml
wmeyer has joined #ocaml
Arsenik has joined #ocaml
jpdeplaix has joined #ocaml
_habnabit has joined #ocaml
bkpt has joined #ocaml
Simn has joined #ocaml
smondet has joined #ocaml
_andre has joined #ocaml
mye has joined #ocaml
thomasga has joined #ocaml
wormphlegm has joined #ocaml
madroach has joined #ocaml
tchell has joined #ocaml
dtg has joined #ocaml
osnr has joined #ocaml
asmanur has joined #ocaml
hyperboreean has joined #ocaml
logicgeezer has joined #ocaml
yroeht1 has joined #ocaml
ttm has joined #ocaml
balouis has joined #ocaml
MarcWeber has joined #ocaml
NaCl has joined #ocaml
buddyholly has joined #ocaml
gnuvince has joined #ocaml
rednovae_ has joined #ocaml
rks`_ has joined #ocaml
maxibolt has joined #ocaml
patronus has joined #ocaml
demonimin has joined #ocaml
orbitz has joined #ocaml
Nahra_ has joined #ocaml
weie has joined #ocaml
contempt has joined #ocaml
mathieui has joined #ocaml
pr has joined #ocaml
mrvn has joined #ocaml
metasyntax has joined #ocaml
levi has joined #ocaml
PM has joined #ocaml
j0sh has joined #ocaml
rixed has joined #ocaml
whitequark has joined #ocaml
mehdid has joined #ocaml
cdidd has joined #ocaml
pango has joined #ocaml
vpm has joined #ocaml
sgnb has joined #ocaml
xaimus has joined #ocaml
rwmjones has joined #ocaml
so has joined #ocaml
zzz_ has joined #ocaml
ohama has joined #ocaml
adrien has joined #ocaml
xenocons has joined #ocaml
tianon has joined #ocaml
Asmadeus has joined #ocaml
davekong has joined #ocaml
iZsh has joined #ocaml
tlockney has joined #ocaml
talzeus_ has joined #ocaml
olasd has joined #ocaml
ggherdov has joined #ocaml
flux has joined #ocaml
Ptival has joined #ocaml
Leonidas has joined #ocaml
ccasin has joined #ocaml
chris2 has joined #ocaml
ivan\ has joined #ocaml
mfp has joined #ocaml
bernardofpc has joined #ocaml
gbluma has joined #ocaml
lopex has joined #ocaml
cthuluh has joined #ocaml
def-lkb_ has joined #ocaml
willb1 has joined #ocaml
tizoc has joined #ocaml
bobry has joined #ocaml
noplamodo has joined #ocaml
caligula__ has joined #ocaml
dezzy has joined #ocaml
Qrntz has joined #ocaml
vbmithr has joined #ocaml
ia0 has joined #ocaml
bacam has joined #ocaml
Jenza has joined #ocaml
Cypi has joined #ocaml
deavid has joined #ocaml
gereedy has joined #ocaml
troydm has joined #ocaml
lusory has joined #ocaml
jave has joined #ocaml
quelu_ has joined #ocaml
wagle has joined #ocaml
alexey has joined #ocaml
Armael has joined #ocaml
pippijn has joined #ocaml
fds_ has joined #ocaml
aggelos__ has joined #ocaml
ski has joined #ocaml
rossberg__ has joined #ocaml
Khady has joined #ocaml
cross has joined #ocaml
samebchase has joined #ocaml
nicoo has joined #ocaml
thelema has joined #ocaml
stomp has joined #ocaml
SuperNoeMan has joined #ocaml
gasche has joined #ocaml
emias has joined #ocaml
cow-orker has joined #ocaml
adrien_oww has joined #ocaml
lenstr has joined #ocaml
josch_ has joined #ocaml
Simn has quit [Ping timeout: 276 seconds]
bitbckt has quit [*.net *.split]
yroeht1 has quit [*.net *.split]
buddyholly has quit [*.net *.split]
maxibolt has quit [*.net *.split]
levi has quit [*.net *.split]
mehdid has quit [*.net *.split]
rixed has quit [*.net *.split]
ivan\ has quit [*.net *.split]
mfp has quit [*.net *.split]
noplamodo has quit [*.net *.split]
simn__ has joined #ocaml
clog has joined #ocaml
<Drup>
(BatSeq, manly)
<Drup>
(and ropes for the svg backend)
<pippijn>
I wonder if js_of_ocaml has string length limits
ollehar has quit [Read error: Operation timed out]
<Drup>
js probably has
fds_ is now known as fds
* wmeyer
is going to buy an FPGA
<pippijn>
wmeyer: what are you going to code in it?
<wmeyer>
pippijn: just for learning
<wmeyer>
and I have quite few ideas
<pippijn>
like what?
<wmeyer>
custom hardware description language :-
<pippijn>
you don't like system-c, verilog and vhdl?
<wmeyer>
and apart from that I work at cores group and know so little about hardware at the moment
<pippijn>
I didn't really like vhdl, but it was ok
<Drup>
wmeyer: I had a project where we designed a high level synthesis tool with some DSL, it was fun :D
<Drup>
(in M1)
<wmeyer>
these languagaes are clumsy
<pippijn>
wmeyer: implement an ocaml compiler accelerator in hardware :)
<wmeyer>
that interprets lambda? possible and would be cool
<Drup>
a spoc for FPGAs ! :D
<wmeyer>
actually that's what my friend does pippijn (almost)
<Drup>
(good luck with that x)
<wmeyer>
Drup: thank you =)
<wmeyer>
I found that hardware has some space for research, but computer science sadly, become a well explored area
<wmeyer>
especially the compiler and programming languages space
<pippijn>
wmeyer: heh?
k3VB6u4d is now known as goodmanio
<Drup>
wmeyer: indeed, that's start to be a well explored area, and by very very clever people
<wmeyer>
well, the code generators are known since 60, look what the state of art is, we have fully verified compilers, we have fast code generators described by DSLs, we have programming languages like K to formalize computr languages etc.
<wmeyer>
that makes me feel awkward
<wmeyer>
and systems like Coq are just awesome, but to be honest I it goes to the edge, what can be a general purpose language
<wmeyer>
(dependent types and proving in one)
<wmeyer>
now, there is good bias going towards domain specific languages
imalsogreg has joined #ocaml
<wmeyer>
Drup: I agree, and tend to say that this heaven for programmers will not last that long!
<Drup>
wmeyer: the area is well explored from a research perspective, not from the practical point of view
<Drup>
just look at the difference between state of the art GC and GC used in practice by "modern" (*gough*) programming languages
<wmeyer>
Drup: seconded, but I am not interested in implementing 100% working system actually, i am more interested in describing idea and having a fun
<wmeyer>
Drup: I can see this
<wmeyer>
Drup: still somebody needs to write this C or C++ ;)
<Drup>
wmeyer: oh yeah, it's probably the funniest part :D
<levi>
There have been some research prototypes for low-level systems programming in safe languages, but they all tend to die after someone gets a Ph.D.
<wmeyer>
levi: I hope someday we will get out of this engineering bagage, and implement second Linux in OCaml or Coq.
<Drup>
levi: well, there is still ats
<Drup>
wmeyer: linux in Coq ? I don't think it's reasonably possible :/
<wmeyer>
but the lifecycle of programs is long: easy to change, cheap to store, and if works stays forever.
<wmeyer>
Drup: you might think like this, but why actually not? Using verfied DSLs and code generators?
<wmeyer>
Drup: ats is a DSL for system programming in fact
<levi>
Many embedded systems vendors supply tools for doing code generation from formal specifications, typically in something nasty like SysML.
<wmeyer>
levi: i quikcly checked, i read OMG and then resembled they designed CORBA and say thank you to myself
<levi>
I imagine it works something like the code extraction feature of Coq, except that you end up with some sort of C/C++ code to implement a state machine.
<levi>
Most practical systems right now use model checking rather than theorem proving, though.
<wmeyer>
because there is abstraction leak from the actual hardware design constraints upwards the language it's defined in
<levi>
I think it's mostly because you don't have to know how to write proofs to run a model checker.
<wmeyer>
I see
<levi>
It just explores the state space specified by your model and looks for counterexamples to your specified properties.