<menace>
a little bit more, and perl will be replaced by ocaml, as my new scripting language =D
menace has quit ["Leaving"]
cjohnson has quit [Connection timed out]
cjohnson has joined #ocaml
<debona|r>
ocaml as a scripting language? Are there any nice regular expression things? or is that not needed with pattern matching?
<monotonom>
str
<monotonom>
I already script much in ocaml.
monotonom has quit ["Don't talk to those who talk to themselves."]
<greenrd>
scripting in ocaml??
* greenrd
's head explodes
smimou has quit ["?"]
<debona|r>
yeah, dammit, everyone who I would like to tell me why they'd choose ocaml over perl for scripting seems to leave before i get the chance
<Smerdyakov>
OCaml is provides far superior support for efficiency in most stages of the software lifecycle.
<debona|r>
but can you as easily do line parsing as you can in perl?
<Smerdyakov>
Yes. If it's hard, write a library to package the nasty stuff.
<debona|r>
hm, very cool. all the more reasons to learn OCaml is good :)
<debona|r>
I was already convinced, but.. :P
lambdawar has quit [Remote closed the connection]
<debona|r>
is there a Net::HTTP type library?
<debona|r>
nm, found something
<debona|r>
no I didn't
yauz_ has joined #ocaml
yauz has quit [Read error: 113 (No route to host)]
ShereKahn has joined #ocaml
<debona|r>
ugh
ShereKahn has left #ocaml []
<debona|r>
"The syntax for labels and optional arguments is confusing, and you may often wonder when to use ~foo, when to use ?foo and when to use plain foo. It's something of a black art which takes practice to get right." I'll say...
<Riastradh>
And it's even worse when you try to think about its interaction with currying.
pac_away has joined #ocaml
cjohnson has quit [Read error: 104 (Connection reset by peer)]
pac_away is now known as pac_
<pac_>
lop
<pac_>
plop
<Smerdyakov>
Now you're in for a trouble.
<pac_>
Smerdyakov: sorry ?
<Smerdyakov>
You should be sorry.
<pac_>
Smerdyakov: what are you talking about ?
<Smerdyakov>
I don't know.
<pac_>
loool
<pac_>
Smerdyakov: are you drunk ?
<Smerdyakov>
I don't know.
<pac_>
lol
<pac_>
is there a difference between OCaml-mode en tuareg mode ?
pac_ has quit ["leaving"]
Herrchen_ has joined #ocaml
eigenspace has joined #ocaml
Herrchen has quit [Read error: 110 (Connection timed out)]
<debona|r>
so is there a net type library ?
lambdawar has joined #ocaml
monotonom has joined #ocaml
mrsolo has joined #ocaml
eigenspace has quit ["Leaving"]
monotonom has quit ["Don't talk to those who talk to themselves."]
ionOS has joined #ocaml
Herrchen_ is now known as Herrchen
Snark has joined #ocaml
<debona|r>
# open Unix;;
<debona|r>
# inet_addr_of_string "hotmail.com";;
<debona|r>
Reference to undefined global `Unix'
<debona|r>
what's this mean?
<debona|r>
oops
<debona|r>
wel, what does it mean anyway?
Snark has quit [Read error: 104 (Connection reset by peer)]
buggs^z is now known as buggs
<buggs>
debona|r, you need to load or specify at the commandline unix.cma
mrsolo has quit [Read error: 113 (No route to host)]
kinners has quit [Read error: 110 (Connection timed out)]
gim has quit ["nettoyage de ventilo"]
gim has joined #ocaml
<slashvar[lri]>
Yop
smimou has joined #ocaml
jynxzero has quit [Remote closed the connection]
<lambdawar>
lo slashvar[lri]
<lambdawar>
oi oi
bk_ has joined #ocaml
karryall has joined #ocaml
Snark has joined #ocaml
cjohnson has joined #ocaml
bk_ has quit ["Leaving IRC - dircproxy 1.1.0"]
cjohnson has quit [Read error: 110 (Connection timed out)]
cjohnson has joined #ocaml
skylan_ has joined #ocaml
buggs has quit [orwell.freenode.net irc.freenode.net]
mattam has quit [orwell.freenode.net irc.freenode.net]
ithkuil has quit [orwell.freenode.net irc.freenode.net]
Lemmih has quit [orwell.freenode.net irc.freenode.net]
Lemmih has joined #ocaml
mattam has joined #ocaml
buggs^z has joined #ocaml
skylan has quit [Connection timed out]
CosmicRay has joined #ocaml
Skal has joined #ocaml
menace has joined #ocaml
dan|el has quit [Remote closed the connection]
vezenchio has quit ["Join the fight against drunken calculus: Don't drink and derive!"]
vezenchio has joined #ocaml
dan|el has joined #ocaml
Nutssh has joined #ocaml
pac_away has joined #ocaml
<pac_away>
plop
pac_away is now known as pac_
<dan|el>
plupp
<dan|el>
what news?
<pac_>
eating a muffin and drinking a grapefruit juice
<pac_>
:)
<dan|el>
I don't know how you people can drink that stuff
<pac_>
sorry it is grapefruit + orange juice
<pac_>
ehehe
<dan|el>
slightly better :)
<pac_>
ehhee
<pac_>
dan|el: what's your favorite drink
Skal has left #ocaml []
<dan|el>
thai iced tea, aloe vera (yes, it can be drunk!), and sobe lightning are a few candidates :)
<dan|el>
wait, maybe it's not sobe lightning... let me double check
<dan|el>
yeah, lizard lightning
<dan|el>
the blizz one is pretty good too
<pac_>
thai iced tea --> wtf
Nutssh has left #ocaml []
vezenchio has quit ["Join the fight against drunken calculus: Don't drink and derive!"]
Lemmih has quit [Read error: 104 (Connection reset by peer)]
kosmikus is now known as kosmikus|away
<dan|el>
why wtf on the thai iced tea?
cjohnson has quit [Connection timed out]
cjohnson has joined #ocaml
<pac_>
dan|el: never drink such drink !!
<cDlm>
why ? sounds yummy
<pac_>
cDlm: I've never drink a thai iced tea...
<cDlm>
that would be "drank" then :p
menace has quit [Read error: 110 (Connection timed out)]
<cDlm>
or maybe drunk.
<cDlm>
too hot here, my english skills melt
<pac_>
lol
<pac_>
drunk I think
Snark has quit [Read error: 104 (Connection reset by peer)]
Herrchen has quit [Remote closed the connection]
clog has joined #ocaml
clog has joined #ocaml
gim has joined #ocaml
pattern has joined #ocaml
karryall has joined #ocaml
Snark has joined #ocaml
Riastradh has joined #ocaml
cjohnson has quit [Connection timed out]
cjohnson has joined #ocaml
karryall has quit ["tcho"]
<dan|el>
pac_: where do you live?
<dan|el>
thai iced tea rocks :)
Snark has quit [Read error: 60 (Operation timed out)]
cjohnson has quit [Connection timed out]
cjohnson has joined #ocaml
Nutssh has joined #ocaml
greenrd has joined #ocaml
cDlm has joined #ocaml
<pac_>
dan|el: montreal
magnus-- has joined #ocaml
<magnus-->
hello
<Nutssh>
Hi.
<magnus-->
quick question about the module system: is it possible to do something like private/public without having to repeat the list of functions and types in a module in both the signature and the structure?
<Nutssh>
No. Within the module system, the only way to hide is via signature ascription.
<magnus-->
okay, thanks
<Nutssh>
And the signature is there for you to write the docs in. If it helps, compile with -i that way the ocaml compiler prints out the signatures, you can copy&paste&edit them and put in docs.
<magnus-->
i see
cjohnson has quit [Connection timed out]
cjohnson has joined #ocaml
CosmicRay has quit [Remote closed the connection]
CosmicRay has joined #ocaml
andrewb has left #ocaml []
magnus-- has quit [Read error: 104 (Connection reset by peer)]
cjohnson has quit [Connection timed out]
cjohnson has joined #ocaml
srv has joined #ocaml
cDlm_ has joined #ocaml
cDlm_ has left #ocaml []
monotonom has joined #ocaml
maihem has joined #ocaml
cjohnson has quit [Connection timed out]
cjohnson has joined #ocaml
Nutssh has quit ["Client exiting"]
pac_ has quit [Read error: 104 (Connection reset by peer)]
pac_away has joined #ocaml
pac_away is now known as pac_
<pac_>
re
<greenrd>
monotonom: OK, I read some of those category theory slides. Could you explain to me how pushouts make multiple inheritance better? Sounds cool.
<monotonom>
A class is an object. Subclassing is having a morphism. It follows that multiple inheritance is pushout, especially if you look at the "troublesome diamond".
<monotonom>
Perhaps if you don't have the troublesome diamond, you don't need a pushout, but just a co-product.
<greenrd>
OK... maybe.
<greenrd>
But how does this help with deciding which implementation of a method to run?
<monotonom>
I have also dreamed that a lot of "cross-cutting concerns" and "aspect oriented programming" are actually co-limits.
<greenrd>
Hmm
<monotonom>
It probably doesn't help directly, but it puts the whole issue and debate in perspective.
<greenrd>
So, what does this abstraction buy you? That is my question. What is the advantage of noting these isomorphisms, in practical terms?
<greenrd>
Ah, I see it buys you something non-trivial.
dobrek has joined #ocaml
<greenrd>
Correct me if I'm wrong, but it actually states something that is not necessarily the case in existing languages.
async_ is now known as async
<monotonom>
That's right, existing languages are all very shabby.
<greenrd>
And, serependitiously, I was thinking of making this a rule in my language only yesterday:
<greenrd>
If B,C extend A, and D extends B,C, then for all X which extend B,C, X must extend D.
<greenrd>
Correct? This follows from the definition of pushout, if you are identifying MI with pushouts.
<monotonom>
Yes.
<monotonom>
make it "D extends B,C minimally", i.e., it doesn't add anything new.
<greenrd>
Hmm
<slashvar[lri]>
greenrd: and what happen if you use a kind of set theoretic interpretation of classes (like in semantic-subtyping) ?
<slashvar[lri]>
it works easily for types, why not for type classes ?
<greenrd>
I thinnk... if I understand correctly... that is the approach I am following with my new language.
<greenrd>
So, yes, what happens? You tell me! ;)
<monotonom>
I would say Set is a category and so all this category theory for OOP applies to the set interpretation.
<greenrd>
Hmm... a class is a category and the inheritance relation is a functor? Would that work?
<slashvar[lri]>
monotonom: yes, but, semantic subtyping (as in CDuce for example) is far more simple to construct/understand, it's just as if you use abstract interpretation where you need type inference, type inference is a kind of ai, but much more accurate
<greenrd>
Hmm maybe I assumed understanding where I had none
* greenrd
looks up semantic subtyping
<slashvar[lri]>
(take a look a the paper sematic-subtyping at LICS 2001 or 2002, it is on the cduce site, www.cduce.org)
<slashvar[lri]>
the idea, is that a type represents a set of values (irreductible closed terms) and then subtyping is just set inclusion
<slashvar[lri]>
(and then you can have intersection, union, differences ...)
* greenrd
tries "A Gentle Introduction to Semantic Subtyping" first instead
<slashvar[lri]>
yeah, better ;)
<monotonom>
That works even better with category theory. A type is an object. As for morphisms the following are equivalent: have a morphism T->S; S is a subtype of T; S can be abstract-interpreted to look like T; T can be data-refined to S.
<pac_>
greenrd: lol my cousin wrote this paper lool
<greenrd>
coolness
<slashvar[lri]>
pac_: you're cousin of whom, Alain ?
<pac_>
slashvar[lri]: yep but not a first cousin
<monotonom>
In fact the troublesome diamond A->B, A->C, B,C->D is resolved perfectly. Because -> preserves behaviour, we are guaranteed that D behaves like both B and C, with all conflicts resolved w.r.t. A wherever possible. (In case of unresolvable conflict, D becomes the final object --- the "unimplementable class")
<pac_>
slashvar[lri]: why ?
<slashvar[lri]>
oki, I work a little bit with Alain (I do my phd-thesis with Castagna to)
<greenrd>
Er, yes, in theory.
<pac_>
slashvar[lri]: eheheee
<greenrd>
In practice, I wonder if there could be subtle problems in getting the implementation right.
<slashvar[lri]>
(s/to/too/ ;)
magnus-- has joined #ocaml
<pac_>
slashvar[lri]: j avais qd meme compris :)
<slashvar[lri]>
héhé
<pac_>
slashvar[lri]: I think Alain should have finished is PhD thesis ?
<slashvar[lri]>
nearly, if I remember it will have his "soutenance" (don't know the english word) in september, or something like this
<pac_>
slashvar[lri]: ok ok
<pac_>
slashvar[lri]: you belong to CDuce team too do you ?
<slashvar[lri]>
pac_: yes
<slashvar[lri]>
(I'm working on the security part)
<slashvar[lri]>
and Banana is in the cduce team, also
<pac_>
slashvar[lri]: security ?
<pac_>
slashvar[lri]: security or safety ?
<monotonom>
I like the point of semantic subtyping. When you "subclass", it won't do to just implement or override methods; you must also give a reason why the new implementation behaves like the old.
<gzl>
monotonom: in regular MI, D could not be implemented?
<slashvar[lri]>
pac_: hum, it should be called secrecy or something like this, it's a kind of access control, but at language level
<monotonom>
D may be unimplementable. But then you will notice it and trace the problem back to B and C being incompatible.
<pac_>
slashvar[lri]: ok
<greenrd>
slashvar: Like private methods in Java? Or more advanced?
<monotonom>
But D may also be implementable, in which case if -> preserves behaviour then you know D can't go wrong.
<slashvar[lri]>
greenrd: more in the idea of non-interference (a kind of depencies analysis) and data flow analysis
<gzl>
monotonom: so pushouts solve the problem of D being unimplementable in some cases, or something else as well?
<slashvar[lri]>
(like in flow-caml)
<greenrd>
monotom: According to the slides posted yesterday, "Pushout is a universal property of any two morphisms with a common domain"
<greenrd>
monotonom: Does this imply that it must always be implementable? That the pushout must always exist?
<monotonom>
If B,C are incompatible in the first place, it can't be helped. If they are compatible, then it is clear what D must/mustn't do. Pushout tells you which case you're in.
<monotonom>
If your category is complete --- in particular, if you have a final class representing the "unimplementable class", then pushouts always exist.
<monotonom>
This is also the same reason why in all sane languages of specifications, you are allowed to express unimplementable specifications, e.g., "I want x<0 and I also want x>0".
<monotonom>
(You can't express that in a programming language.)
<slashvar[lri]>
monotonom: as for the bottom type for subtyping
<greenrd>
I have a possibly radical idea.
<monotonom>
Yes, that is the bottom type.
<greenrd>
One can define a subtype in which the precondition for a method is always false.
<greenrd>
I argue that's OK, as long as the method is never called on objects of that type.
<monotonom>
I have to do some other things for half an hour now.
<greenrd>
To take that to an extreme, one could even instantiate objects where all methods have impossible preconditions.
<greenrd>
As long as one doesn't call any methods on those objects :)
<greenrd>
(Of course the constructor would have to have a satisfiable precondition, but I didn't mean to classify constructors as methods in this context.)
<greenrd>
The "unimplementable type" could be just such an object.
<greenrd>
Wait.
<greenrd>
Sorry, in my haste I was lax: The "unimplementable type" could be just such a type, I meant to say.
<greenrd>
Now the punchline: The unimplementable type is the type of the null pointer!
<greenrd>
As long as all object references are allowed to refer to null, I think that works.
<Smerdyakov>
I don't like having object references refer to null.
<Banana>
ho ho...
<greenrd>
Well, yes, it is messy. In existing languages. However, if you have a verifying compiler, you can guarantee no null pointer exceptions.
<Banana>
the unimplementable type should be uninhabited i think...
<greenrd>
Do you see?
<greenrd>
By "verifying compiler" I mean one that verifies proofs that invariants, preconditions and postconditions are always satisfied in any program run (on working hardware, obviously).
<greenrd>
If preconditions are always satisfied on every method call, and if nulls are objects which implement all methods with impossible preconditions, then there can be no null pointer dereferences. Simple logic.
<greenrd>
Woohoo, this is incredibly cool!
<Riastradh>
...now prove that there are no null pointer dereferences.
<slashvar[lri]>
hum ...
<Riastradh>
(well, write the code that will prove that)
<slashvar[lri]>
it is like proving that the type referenced is empty
<greenrd>
Well, obviously the whole proof system will be a challenge. According to Tony Hoare noone has done a verifying compiler for a serious language since the 1960s.
<Riastradh>
(er, write the code that proves all those preconditions)
<greenrd>
That's a goal of mine, to do that.
<Riastradh>
What do you define as a 'verifying compiler?'
<slashvar[lri]>
greenrd: yes, in presence of aliasing it's not realy possible
<slashvar[lri]>
so ...
<dobrek>
Riastradh: compiler which assumes preconditions and proves invariants and postconditions.
<Riastradh>
That is, what preconditions & postconditions constitute a 'verifying compiler?'
<dobrek>
Riastradh: If I understand well, smthing like www.eschertech.com are trying to do.
<greenrd>
(There was a registration-free link I found but I've lost it :(
<slashvar[lri]>
dobrek: the problem is more in code generation, precondition & postcondition is not so hard to check (it's depend on the logic used)
<Riastradh>
greenrd, you said what you meant by 'verifying compiler,' but you didn't specify any preconditions.
<greenrd>
Why is it not really possible in the presence of aliasing?
<greenrd>
The preconditions, postconditions AND PROOFS are all written by the programmer in my vision. At least, at first.
<greenrd>
There is obviously scope for mechanical assistance.
<Riastradh>
I see.
<dobrek>
slashvar[lri]: what do you mean here as code generation?
<dobrek>
I think you are suppose to write this conditions, by hand.
<slashvar[lri]>
dobrek: the real problematic parts are in the code generation phase of the compiler (ie source to machine code), otherwise, some kind of type system can protect you from runtime exception (it's depand on your language, of course)
<greenrd>
It seems they have beaten me to it though.
* greenrd
needs to wikify all this info... this is interesting stuff
<Smerdyakov>
greenrd, can you summarize the interesting stuff? (I am coming late to this conversation.)
<pac_>
Design by Contract like in D language
<pac_>
interesting
<dobrek>
slashvar[lri]: ok, but this is hard part of every compiler.
<Smerdyakov>
I believe my advisor has written a system that essentially allows use of GCC as a verifying compiler.
<greenrd>
Smerdyakov: Yes, I plan to summarise some of this discussion on a wiki.
Snark has joined #ocaml
<greenrd>
Smerdyakov: Really? How are the post/pre conditions specified?
<Smerdyakov>
Macros with C expressions as arguments
<greenrd>
Link?
<Smerdyakov>
Nope. :)
<greenrd>
Ah, not published yet?
<Smerdyakov>
Right. Not even considered interesting enough to call "research," either, as far as I know.
<greenrd>
That's odd.
<Smerdyakov>
This is really quite a "solved problem."
<Smerdyakov>
Axiomatic semantics imply the whole technique.
<greenrd>
Yes, I was suspicious of Tony Hoare's claim that it was a Grand Unsolved Challenge.
<dobrek>
Smerdyakov: There exist no tool for any popular language to do it.
<Smerdyakov>
dobrek, it's painful to do.
<Smerdyakov>
(where "do" means "implement")\
<Smerdyakov>
And, again, I believe we have a tool for C, which surely qualifies.
<greenrd>
I can imagine... especially with C and gcc - double gack!
<dobrek>
Smerdyakov: I guess, and I guess that if it was suppose to run in a reasonable time it would require user to specify so many artificial conditions to halp the prover that it would be unresonable again to use
<monotonom>
greenrd's dream is also my dream.
<dobrek>
sorry halp means help
<greenrd>
Considering the bullshit that passes for research in some subfields of copmuting, I would think it is far too modest of your advisor for him to say it is not research!
<dobrek>
Smerdyakov: I would love to see, it almost as much as I would love to use it in work.
<greenrd>
I would love to see it too.
<Smerdyakov>
He hasn't said that, but he also hasn't mentioned any plans to publish a paper just on it.
<greenrd>
A clarification: it generates proofs itself? Or it requires the user to write them?
<greenrd>
And the pre/post can be arbitrary C expressions?
<dobrek>
In my company we developed a framework for design by contract for c++ and I must say that for this sort of language this is only resonable solution I know.
<dobrek>
but we never tried to make any prove on it.
<Smerdyakov>
It generates preconditions/loop invariants/etc. in the assembly code, and then you can use your decision procedure of choice to analyze it.
<slashvar[lri]>
if you're interest in that kind of things, there's also some tools based on coq proof assitant (hum something like "why" and "cracatoa")
<slashvar[lri]>
(cracatoa is for java, but I think they have things for C)
<slashvar[lri]>
(and for ocaml ;)
<greenrd>
Smerdyakov: I don't follow. In my understanding, preconditions must be written by the programmer, because only the programmer knows the semantics intended.
<greenrd>
Although, of course intermediate facts can be derived from those specified.
<Smerdyakov>
greenrd, preconditions in C code are different from preconditions in assembly code.
<greenrd>
Oh, sorry, you already said that they're specified as macros.
<Smerdyakov>
There's also a big difference between C variables and assembly operands.
<greenrd>
Right
<greenrd>
I'm just trying to understand what it does... my underlying question is does it have any limitations on what it can verify?
<Smerdyakov>
Anyway, if you just want to verify at the C level, things are trivial.
<greenrd>
Presumably it must have in theory, because of the halting problem.
<Smerdyakov>
I am talking about a way to augment a C compiler to keep invariants around in a useful form at the assembly level.
<Smerdyakov>
There is no verification involved in that tool.
<Smerdyakov>
You can then apply various techniques.
<greenrd>
Oh, I think we have been misunderstanding each other then!
<Smerdyakov>
Verifying assembly code is trivial with appropriate decision procedures.
<slashvar[lri]>
Smerdyakov: there's some problems with aliasing, even if you use precondition (one of my adviser made some precondition-proof on O2C, an kind of C for O2 OODB, and encounter decidability problems ... )
<Smerdyakov>
This is what proof-carrying code has done since the beginning.
<monotonom>
Even coming up with "useful" invariants is hard enough. Of course when has the halting problem halted anyone?
<Smerdyakov>
slashvar[lri], that depends on which sorts of things you want to prove.
<slashvar[lri]>
yeah
<greenrd>
Yes the halting problem only applies to infinite machines, which don't exist ;)
<slashvar[lri]>
(but we begin with problem of null-pointer derefencing ... )
<dobrek>
Smerdyakov: This guys from ASTREE are doing similar veryfication for C, but withou goto, recursion, recursive types and smthing alse so I don't beleave it is so trival.
<greenrd>
However for all practical purposes the halting problem exists.
<Smerdyakov>
slashvar[lri], which is why C is no fun here.
<Smerdyakov>
dobrek, it depends critically on the facts you want to prove....
<dan|el>
what is this "troublesome diamond" ?
<Smerdyakov>
dobrek, if it's something with a type safety flavor, this really _is_ trivial, generally.
<monotonom>
There is no halting problem if we treat programming scientifically, i.e., the burden of proof is upon the author.
<slashvar[lri]>
(hum time to go back home ... see you later ;)
<Smerdyakov>
monotonom, thankfully, we can automate most proof generation.
<monotonom>
Yes, I actually don't worry about the halting problem in practice.
<greenrd>
dan|el: When B,C inherit from A, and D inherits from B,C, there is allegedly a "troublesome diamond". There are different views about what the semantics of this should be.
<monotonom>
The thing is in the real world programs are written with purposes, and the purposes are not too hard to guess.
<greenrd>
monotonom: I agree, burden of proof is on the author. If the author cannot prove their code they don't understand it well enough.
<monotonom>
As well, they are even sometimes written with good structure.
<greenrd>
Shocking, isn't it?
<Smerdyakov>
You don't really need an idea of "purpose" to do effective inference for useful theories.
<dan|el>
greenrd: thank you
<Smerdyakov>
Effectively, the programmer only needs to specify inductive hypotheses.
<Smerdyakov>
We have well-studied techniques to fill in the rest.
<dobrek>
Smerdyakov: I understan now, I guess what you mean.
<magnus-->
is there any function that takes a string and returns an in_channel that reads from the string?
<greenrd>
oh, back to reality ;)
<slashvar[lri]>
magnus--: hum ... sprintf or something like this ...
<slashvar[lri]>
;)
<dobrek>
magnus--: there is no. And this sucke becouse my unit test are evolving into Testcase
<dobrek>
magnus--: for this exactly reason.
<magnus-->
ack
<magnus-->
:/
dobrek has quit ["leaving"]
dobrek has joined #ocaml
<greenrd>
Smerdyakov: I seem to remember that any first-order logic proposition is decidable. In real-world cases of program specifications, is it always going to be decidable in a reasonable time? I think the answer is no, and I think that's why it's not so trivial as you make it out to be.
<greenrd>
Apologies if my terminology is wrong.
<slashvar[lri]>
magnus--: maybe something with stream ...
<magnus-->
slashvar: i'll try and see if i can find something
<slashvar[lri]>
but, is transforming a string into an in_channel very usefull ?
<slashvar[lri]>
take a look also at sscanf
<dobrek>
magnus--: tell me if you find something
<slashvar[lri]>
so ... i'm going home now
<dobrek>
slashvar[lri]: for simple unit tests it could be.
slashvar[lri] is now known as slashvar[home]
<Smerdyakov>
greenrd, the theories you care about are often decidable.
<Smerdyakov>
greenrd, ... in reasonable time.
<Smerdyakov>
Overly complicated theories probably won't be used informally by programmers in understanding their code.
<magnus-->
Streams seem to be the right thing
<magnus-->
to use instead of in_channel
mattam_ has joined #ocaml
Snark has left #ocaml []
<greenrd>
Smerdyakov: I see. Are there many papers on verifying code in imperative languages in the presence of aliasing etc.?
<Smerdyakov>
Yes.
<greenrd>
I would like to read the prior work.
<greenrd>
Could you point me in the right direction?
<Smerdyakov>
A common approach is to perform an alias analysis and use that to guide insertion of disjunctions (over possible alias relations) during verification.
<greenrd>
Could you suggest some paper(s), for someone whose knowledge of the area is limited?
mattam has quit [Read error: 110 (Connection timed out)]