<schlick>
vodka-goo: twelf isn't practical for programming, nor is mizar. twelf, if memory serves, doesn't try to prove anything, it only checks proofs already made. Mizar works strictly on traditional mathematics. You could bludgeon a program into it but it would probably be about as much work as writing your own prover, I gather.
<schlick>
I have found one more since I listed them. It's called Elf.
<schlick>
So the list as it stands is: ACL2, Coq, Elf, Isabelle, and MetaPRL. I didn't list some obsolete provers, these are only the latest descendants.
<schlick>
Some of the others mentioned on Wikipedia's "automatic theorem proving" page I can't make out. There's one called Phox they say works on ML programs but the documentation doesn't seem to indicate such.
<vodka-goo>
I don't know the difference between twelf and elf (isn't elf the old version ?), but I think both perform proof search
<schlick>
I don't think they're related no.
<schlick>
Elf is designed specifically for proofs of programs.
<schlick>
It's apparently quite obscure. Order of popularity (most to least) seems to be Coq, ACL2 <beyond here we get quite obscure> Isabelle, MetaPRL, and Elf.
<schlick>
Still, nice to know your options and compare implementations.
<schlick>
Odd that model checkers seem to be so much more popular.
<schlick>
Hmm, you seem to be right. Twelf looks like the descendant of Elf. The wikipedia page is a bit misleading.
joshcryer has joined #ocaml
<vodka-goo>
model checking is easier to understand, so many more people search in that way, and many users prefer it
<schlick>
Gah. Now the wikipedia page looks fine. I must be getting confused somewhere. :(
<schlick>
Well, the downside of model checking is it doesn't scale nearly as well.
<vodka-goo>
but model checking is restricted and doesn't scale easily
<vodka-goo>
:)
<schlick>
One thing I haven't gotten confirmed is whether a theorem prover can generate a counter example or not.
<vodka-goo>
on this agreement, I wish you good night
<vodka-goo>
schlick: usually no
<schlick>
If it can't, that's a real problem. On the other hand surely some blend could be better. For instance, to try to only use a model checker when you know a rule has been violated.
<vodka-goo>
coq doesn't, twelf probably doesn't either
<schlick>
I don't understand why it's not possible.
<vodka-goo>
actually, coq doesn't generate anything (automated proving in coq is very restricted)
<vodka-goo>
schlick: sometimes there is no counterexample to a non-provable formula
<schlick>
It seems like if you say "this is the set of valid input/preconditions" "these are the invariants and postconditions" it could solve for the (possibly empty) set of things that fall outside the invariants and postconditions given the preconditions.
<vodka-goo>
there could be counterexample generation as a hack/heuristic however
<schlick>
Oh I understand why it can't generate something if it can't disprove it.
<schlick>
But if it /can/ disprove it it seems like it should be able, at least in theory.
<vodka-goo>
if it can disprove it then you've got an example (at least in coq/lf where the logic is constructive)
<schlick>
So it can generate a counter example in that case?
<vodka-goo>
a proof of the negation is a counter-example
<vodka-goo>
but probably not the kind of thing you want
quamaretto has quit [Connection timed out]
<vodka-goo>
I'm not sure
<vodka-goo>
anyway, gotta go
vodka-goo has quit ["Connection reset by by pear"]
raziel_ has joined #ocaml
Raziel has quit [Read error: 110 (Connection timed out)]
* Smerdyakov
appears.
raziel_ is now known as Raziel
<schlick>
Smerdyakov: have time to talk some more?
batdog|gone is now known as batdog
batdog is now known as batdog|gone
exa has quit [Remote closed the connection]
ski__ is now known as ski_
rq has quit ["Leaving"]
shirogane has joined #ocaml
ski_ has quit [Success]
<Smerdyakov>
schlick, OK.
<Smerdyakov>
schlick, maybe off and on responsiveness. :)
Snark has joined #ocaml
Raziel has quit ["Yo soy goma. Tú eres cola."]
<schlick>
Smerdyakov: after you pointed out Coq to me I went back and looked for other program-oriented theorem provers that are open source, currently my list includes: ACL2, Agda, Coq, Isabelle, LEGO, MetaPRL and Twelf. Do you know of any others to look at?
<Smerdyakov>
PVS? I don't know if it's "program-oriented."
<schlick>
PVS is, but it's closed source.
<Smerdyakov>
I don't think I know of any others.
<schlick>
One other thing I'm curious about...
<schlick>
I've been reading about the relationship between theorem provers and model checkers. I've seen some papers claim a theorem prover (as in any of them) can't generate a counter example when they prove something false. Is this so? And if so, why is it impossible. It seems like it should be possible to me.
<schlick>
[relevency is that model checkers can, how is pretty obvious to me]
<schlick>
The reason I care is it makes figuring out how you screwed up a lot easier if you have a example of input that would cause misbehavior.
<Smerdyakov>
There is nothing fundamental about theorem provers that makes them unable to generate "counterexamples." Many do.
<Smerdyakov>
Just not usually this kind of higher-order logic based provers.
<Smerdyakov>
Especially with constructive logic, where it's _not_ the case that even absolute non-provability implies the existence of "a counterexample."
<schlick>
It made sense to me that they should be able to. It seems like you'd "just" be solving for the set that falls outside the allowed range (I understand "just" would be nontrivial).
ski has joined #ocaml
<schlick>
It is true that theorem provers tend to perform quite a bit better, correct? They would be a better choice when either could work?
<Smerdyakov>
Do you understand that the lack of a proof doesn't imply the existence of a proof of the negation in constructive logic?
<schlick>
I understand that not being able to prove something is not the same as proving it false, which I believe is what you're asking.
<Smerdyakov>
Not entirely. A counterexample is a kind of proof of the negation of a proposition.
* schlick
nods.
<Smerdyakov>
In other words, if you always either return "it's true" or "here's a counterexample," then clearly you have a decision procedure, right?
* schlick
nods.
<Smerdyakov>
But we know that all interesting logics have undecidable entailment problems.
<schlick>
Yes, if it can do arithmetic it's undecidable.
<Smerdyakov>
You have to be careful in saying that. There are decidable arithmetic theories, like Presburger Arithmetic.
<Smerdyakov>
(Which is an expansion of linear arithmetic, which everyone knows is solvable via off-the-shelf linear programming solvers today.)
pango_ has joined #ocaml
<schlick>
Was just parroting what I've read, which is what everybody brings up as soon as you mention trying to statically check things, that Godel's incompleteness theorem shows that it isn't always possible thus we should all give up and not check anything. :P The explanations I've heard are that if a logic is capable of doing basic arithmetic it is undecidable. Maybe that's not true.
<schlick>
capable of doing basic arithmetic it is undecidable. Maybe that's not true.
<Smerdyakov>
That depends critically on your definition of "basic."
<schlick>
I've never heard it specified but I'd take it to mean addition and subtraction.
<Smerdyakov>
No, just addition and subtraction in first-order logic is decidable.
<Smerdyakov>
You need multiplication (at least) to get into the interesting stuff.
<schlick>
Isn't multiplication just repeated addition?
<Smerdyakov>
And isn't the halting problem just figuring out if a program terminates?
<Smerdyakov>
Multiplication isn't first-order definable from only addition and subtraction.
<schlick>
I thought it was definable using only those things.
<schlick>
A * B means add A to A B number of times... Or so I thought.
<schlick>
I probably didn't word that too well since it makes the situation of A * 1 sound odd but you know what I ment.
<Smerdyakov>
It turns out that any reasonable axioms that you think of admit alternate interpretations... the strange area of "nonstandard arithmetic."
<schlick>
And that's where the decidibility problem comes from?
<Smerdyakov>
Well, any first-order definable theory is decidable.
<Smerdyakov>
By enumerating & checking all possible proofs
pango has quit [Read error: 110 (Connection timed out)]
<schlick>
I take it that's not true in constructive logic.
<Smerdyakov>
It's even more true in constructive logic, but you have a different notion of truth that admits strictly fewer true facts.
<schlick>
So saying whether something is true or not gets harder.
<schlick>
In general.
<Smerdyakov>
Not necessarily.
rq has joined #ocaml
<schlick>
Guess I'm having trouble telling where the problem comes in then.
<schlick>
But that's ok, it doesn't sound like it's tied to the original topic too tightly, more to math in general than verification.
<schlick>
Basically apparently it's possible for theorem provers to generate counter examples most of the time.
<Smerdyakov>
No.
<Smerdyakov>
It's intractable in most cases when you go beyond first-order logic.
<Smerdyakov>
And when you use constructive logic.
<schlick>
So normally they can't?
<Smerdyakov>
I don't know of any higher-order logic theorem prover or proof assistant that has any counterexample generation facility.
<Smerdyakov>
You usually only find that for first-order provers.
<schlick>
Ok.
<schlick>
The other thing I've read is model checkers are generally far slower and consume more processor time and memory than theorem provers. Given getting a counter example is often important to fixing the flaw, would it make sense to try to use a theorem prover normally, and then use a model checker only if you found a problem?
<Smerdyakov>
It's always preferable to integrate correctness guarantees as closely as possible with your development process.
<Smerdyakov>
I think that dependently typed programming, where programs that don't satisfy your specification don't type check, is the way to go.
<schlick>
Given dealing with the halting problem means being able to tell the checker to "assume" something can occur, or feeding it additional proof steps, does dependent typing catch all the bugs with the exception of that problem?
<schlick>
Sorry if I'm not able to state it more clearly. What I'm getting at is yeah, it's great to not have to worry about the size of a variable, and make sure that I'm not writing to constants, or doing math with half string half numbers (and ending up with who knows what as a result), but most of the serious problems in programming have to do with the relationship between variables, or the specific values of them.
<Smerdyakov>
Read that series of books I recommended and you will understand. :)
<schlick>
programming have to do with the relationship between variables, or the specific values they hold, not just assuring they fit in a broad range based on storage space.
<schlick>
I'll have to wait. I'll probably buy them but I need to get the money together.
<schlick>
I'd like to know if it solves my problem or not.
<schlick>
I want to be able to say things like "This function cannot be called while I is set to 5, or while B is 1 and C is 3" and have it statically checked.
<schlick>
Or be able to say X can only be one of 1 5 and 9.
<schlick>
And statically check that.
<Smerdyakov>
Sure. You have a narrow view of what type systems are.
<schlick>
Yes. All I've ever seen the word "type" tacked onto is things like in C and C++ (and similar systems) where you can basically set a variable read only, and have to say how much space to allocate, which is really not terribly useful. CQual is the first thing I've seen to have more useful (and significantly more odd, to me) types.
<schlick>
I'm also told that a object can be viewed as a "type".
<schlick>
Object in the "object oriented programming" sense.
<schlick>
And I suppose now that I think about it I should have said class, not object.
<schlick>
Smerdyakov: Are there any languages you know of that demonstrate types that can do the sort of things I mentioned?
<Smerdyakov>
Coq
Snark has quit ["Leaving"]
<schlick>
Hadn't considered that a language but I suppose that'd work.
<schlick>
I'll be getting the books you mentioned, it's some encouragement knowing there's some light at the end of the tunnel.
<Smerdyakov>
I haven't used any others, but there are some I've heard of, like Epigram.
<Smerdyakov>
(And I'm sure the other proof assistants that you listed that are base on constructive type theory also fit the bill.)
<schlick>
I wonder why such things aren't more widely used. Maybe the motivation isn't there with EULAs keeping companies from being sued, and I guess you can use bugs to sell updated versions.
* schlick
looks for Epigram.
<schlick>
Hey this is neat.
<schlick>
Any theories on why this stuff isn't more widely used?
<schlick>
Even has tutorials here.
lispy has quit [Remote closed the connection]
lispy has joined #ocaml
Skal has joined #ocaml
MisterC has joined #ocaml
Snark has joined #ocaml
descender has quit [Remote closed the connection]
descender has joined #ocaml
Skal has quit [Read error: 110 (Connection timed out)]
rq has quit ["Leaving"]
shirogane has quit [Read error: 104 (Connection reset by peer)]
vodka-goo has joined #ocaml
rq has joined #ocaml
Skal has joined #ocaml
MisterC has quit [Read error: 110 (Connection timed out)]
vodka-goo has quit ["Connection reset by by pear"]
pango_ has quit [Remote closed the connection]
pango has joined #ocaml
<pango>
flux__: looks neat... I wonder how effective it is however, invariants are often temporarily broken (will need to read on used detection techniques)
<flux__>
I guess it's something that doesn't really tell you (the developer) anything new (useful), but atleast maybe it serves as a way to generate loads of onvariants (which you intuitively can check) and then keep the code working during modifications ;)
<flux__>
no, I haven't tried it
Raziel has joined #ocaml
ppsmimou has joined #ocaml
pingoo has joined #ocaml
m3ga has joined #ocaml
revision17_ has joined #ocaml
Revision17 has quit [Read error: 110 (Connection timed out)]
Snark has quit ["Leaving"]
ramkrsna has left #ocaml []
ppsmimou has quit ["Leaving"]
m3ga has quit ["disappearing into the sunset"]
rillig has joined #ocaml
joshcryer has quit [Connection timed out]
<rillig>
I have a little problem.
<rillig>
# open Str;;
<rillig>
# regex "foo";;
<rillig>
Unbound value regex
<rillig>
(I'm completely new to OCaml. :))
<juri>
it's regexp, not regex :-)
<rillig>
# regexp "foo";;
<rillig>
Reference to undefined global `Str'
<rillig>
ok, found it.
<rillig>
"ocaml str.cma" worked.
<rillig>
thanks
rillig has quit ["exit(EXIT_SUCCESS)"]
<juri>
oh, i didn't have time to suggest using ocamlmktop. oh well.
_fab has joined #ocaml
Bigb[a]ng is now known as Bigbang
SnarkBoojum has joined #ocaml
SnarkBoojum is now known as Snark
<schlick>
flux__: Thanks (I was asleep when you mentioned Daikon). That really is neat. I think the main way it would be used is programmers tend to know how you're "supposed" to use what they wrote. It causes problems in finding bugs because bugs tend to happen when you do something the programmer didn't think of. The programmer could use this to get a list of invariants that describe proper program behavior, then
<schlick>
programmer could use this to get a list of invariants that describe proper program behavior, then feed it to a theorem prover or model checker.
joshcryer has joined #ocaml
<flux__>
schlick, btw, www.splint.org might also interest you
<flux__>
although that might not be anything special with a language that has strong typing and saner syntax
batdog|gone is now known as batdog
<vincenz>
heh, schlick still asking? :P
<dylan>
different question, I perceive.
Raziel has quit [Read error: 104 (Connection reset by peer)]
Raziel has joined #ocaml
Raziel has quit ["Yo soy goma. Tú eres cola."]
__DL__ has joined #ocaml
Raziel has joined #ocaml
<schlick>
I haven't been asking anything today, I have a pretty nice collection of things to look at.
smimou has joined #ocaml
<schlick>
flux__: I knew about Splint already. It is interesting though. Most of the research work gets done on C and Java, despite their flaws. I'm not sure why there's the near absence of C++ research. If I had to guess it'd be due to the insane complexity of the language.
gim has quit ["tchoo"]
<Smerdyakov>
More research work gets done on formal methods for functional languages; it's just that that's not so much done in the USA.
<schlick>
flux__: I consider C analysers interesting because C does so little sanity checking you get a good idea of what the kinds of checking you can do, are. Basically everything has to be added on top of C. If you're new to this sort of thing it helps you pick out things to read about.
<Smerdyakov>
...and perhaps it's less likely to yield usable tools.
<Smerdyakov>
schlick, you think that's interesting? My thesis research is on checking machine code. :)
<schlick>
I would think functional languages (at least fairl pure ones, would be easier.
<schlick>
Smerdyakov: I've seen two mentions of such things, but no articles on it. I never could see how it was possible other than say, via a verifiying compiler, given that all you have is raw memory read/writes, telling what the programmer "ment" in raw assembly would be pretty hard.
<Smerdyakov>
We don't usually try to prove "full correctness" today. Instead, we focus on specific properties, like memory safety.
<schlick>
Smerdyakov: I am extremely interested in the talk you were practicing yesterday. It would be very close to what I'd hope to do for my language. Basically feed the thing into a theorem prover (and/or model checker) automatically, based on source code annotations.
<Smerdyakov>
It's relatively easy to build a certifying compiler for a high-level, type-safe language that outputs binaries with enough proof hints to make checking easy.
<Smerdyakov>
schlick, while I'm trying to convince you to use type systems, you seem to be leaning more toward the conventional approaches, and for that the most visible tool is ESC/Java. Have you looked at it>?
<schlick>
Smerdyakov: That's probably true. There are some projects that do nothing but check for memory leaks (statically, which is actually pretty impressive). However I'd like to have my language only compile if it can verify something based on the assumptions and additional lemmas you provide. Then you can go back and test (only) your assumptions, and if they hold, you're in the clear for all possible inputs.
<schlick>
test (only) your assumptions, and if they hold, you're in the clear for all possible inputs.
<schlick>
Smerdyakov: I'm not writing anything off yet, I'm interested in /all/ my options. Also, CQual is strictly about types, and I find it very interesting, though very hard to wrap my head around. It seems to work somewhat like ML, in that it does type inference. I just don't have much on types yet. I plan to get the books you showed me when Amazon.com starts doing their cheap shipping for Christmas stuff.
<schlick>
showed me when Amazon.com starts doing their cheap shipping for Christmas stuff.
<schlick>
And yes, I'd seen ESC/Java. :)
<flux__>
smerdyakov, btw, didn't the new (beta) java byteloader have some approach that used code certification?
<schlick>
Please don't stop suggesting new things though, I /hadn't/ heard of Daikon, which I find very interesting. It should help you flesh out specifications much better.
<Smerdyakov>
flux__, I don't know much about Java, and I don't know anything about that. :)
Oatmeat|cs has joined #ocaml
Oatmeat|cs has quit [Read error: 104 (Connection reset by peer)]
<Smerdyakov>
schlick, I'm in the CQual office. (The main people working on it are either still there or used to be.) :-)
<schlick>
I really wish people had told me about this sort of thing when I was younger. I had to teach myself /everything/. I started out with some horrible habits. BASIC with goto-only and mandatory line numbers, for example. In highschool, amazingly (considering where we are), they had a BASIC programming class. I turned in the final program, which worked for almost all inputs, was in color, and had musical scores for errors.
<Smerdyakov>
flux__, is this just an extension to the traditional bytecode verifier stuff?
<schlick>
final program, which worked for almost all inputs, was in color, and had musical scores for errors. The teacher couldn't find the cause of the one error we noticed, so gave me a full score. :P It was about 15 pages long. :P
<flux__>
smerdyakov, java 1.6 supposedly will have type checking verifier, to remove the need for runtime checking of permissions
<flux__>
obviously it will need bytecode specifically built for it
<schlick>
Getting out of the goto habit wasn't that bad cause it'd hurt me several times already. Had a awful time wrapping my head around OO though. All the froofroo vague wording doesn't help.
<schlick>
Smerdyakov: BTW, the guy who used CQual on the Linux kernel... If you could, please tell him at least one user appreciates it. I was impressed at how well he handled Al Viro's unnecessary extreme hostility.
<schlick>
Smerdyakov: And thanks for making the tool and its source available for free.
<Smerdyakov>
schlick, Rob Johnson?
<Smerdyakov>
flux__, I don't see any mention of eliding permissons checks -- that would be a big deal. It sounds like they are just using my advisor's invention from the mid-90's (proof-carrying code) without crediting him. :-P
<schlick>
I don't know his name, I just saw the thread on the kernel mailing list. He caught several bugs in filesystem drivers that could have lost users data.
<schlick>
Smerdyakov: Lots of interesting papers one directory up from the one you showed me. Any others you recommend? I find the one on debugging verifying compilers very interesting.
<Smerdyakov>
schlick, no, just that the later you go, the more personally involved I am in the work. :)
<schlick>
If I'm understanding these abstracts right, this means that it's not completely insane to try to check that a compiler for a well designed language produces correct output down to the metal.
<Smerdyakov>
Yeah, that's old news.
<schlick>
Heh, not to me. ;)
<schlick>
Smerdyakov: So you're involved in the BLAST model checker for C too?
<Smerdyakov>
Was a while ago. I must leave again now.
<schlick>
Ok, thanks and take care.
vodka-goo has joined #ocaml
benny has quit ["Leaving"]
benny has joined #ocaml
pango has quit ["Leaving"]
benny is now known as ben|food
pango has joined #ocaml
<kmagdsick>
Hey, are any of you aware of any Ocaml ORM/Webserver/AJAX stacks, similar to Ruby on Rails or TurboGears ?
shirogane has joined #ocaml
KrispyKringle has quit [Read error: 110 (Connection timed out)]
quamaretto has joined #ocaml
rillig has joined #ocaml
<quamaretto>
Rowrbazzle
<ben|food>
turbogears does ajax?
ben|food is now known as benny_
rq has quit ["Leaving"]
Snark has quit ["Leaving"]
ld has joined #ocaml
ld has quit ["leaving"]
samx_ has joined #ocaml
samx_ has quit [Client Quit]
rq has joined #ocaml
_fab has quit []
Bigbang is now known as Bigb[a]ng
__DL__ has quit ["Bye Bye"]
ski has quit [Read error: 110 (Connection timed out)]
Mitar has joined #ocaml
smimou has quit ["bli"]
Raziel has quit [Read error: 110 (Connection timed out)]
joshcryer has quit [Read error: 104 (Connection reset by peer)]
quamaretto has quit ["Chatzilla 0.9.68.5 [Firefox 1.0.7/20050915]"]
Skal has quit [Remote closed the connection]
<kmagdsick>
benny_ : yes, TurboGears does AJAX ... well it prefers to use something other than actual XML for the message protocol, but it is asynchronous javascript
Raziel has joined #ocaml
<benny_>
kmagdsick: cool.... so do you maybe know cheetah templates?
Mitar has left #ocaml []
<kmagdsick>
benny_ : nope on cheetah templates, sorry
<benny_>
aye
<kmagdsick>
benny_ : unless that's another name for kid templates
<kmagdsick>
benny_ : cheetah templates look a fair amount like kid templates
<benny_>
cheetah templates are cool, i'm thinking of copying the idea but using haskell instead of python
rq has quit ["Leaving"]
<schlick>
Can anyone confirm region based memory management always leaks? The MLton page seems to indicate such.
<schlick>
I'm also curious about people's opinion of strict top to bottom, left to right evaluation, as in Smalltalk, instead of following the usual mathematical precedence rules to reorder expressions.
<kmagdsick>
schlick: Avoiding mathematical conventions in evaluating mathematical expressions seems like a nice way to indroduce bugs
<schlick>
I suppose that's so. Lisp seems to do ok. It's just one of those things that seems like it aught not be, kinda like furnature shouldn't have sexes, but european languages insist that they do.
<kmagdsick>
but LISP has parentheses
<kmagdsick>
if you force parenthesies, then there are no surprises
rq has joined #ocaml
<kmagdsick>
I remember, the first thing I wrote in Ocaml was a little program that would log into my router using the http interface
<schlick>
And something happened?
<kmagdsick>
and I wrote the http code myself
<kmagdsick>
as a learning exercise
* schlick
nods.
<kmagdsick>
but I assumed that \ddd character literals were in octal, just like about every other language out there
<kmagdsick>
... which means I wasn't sending \r\n, but a vertical tab and something else
<kmagdsick>
strangely enough, at least at that time, Yahoo's webserver was remarkably liberal with what it accepted
<kmagdsick>
so my http code could get the yahoo front page
<kmagdsick>
but my router was barfing on my malformed http requests
<kmagdsick>
I fired up ethereal and figured it out pretty quickly
<kmagdsick>
but there was some real head-scratching going on for a bit there
<schlick>
That's true...
<kmagdsick>
so I think if you're not going to use standard math order of operations, you should force the use of parentheses
<kmagdsick>
unless you're using an rpn language like Forth
<kmagdsick>
which also has no ambiguity
<kmagdsick>
but with infix notation, you really should use standard order of operations
<schlick>
I'm not sure I'm willing to follow the \ddd or leading-0 = octal, leading 0x = hex, and no notation for decimal and binary C convention. It's totally random and people screw up with it all the time. What I'm planning is for numeric constants you have to specify the base with a suffix b for binary (why nobody has this I don't know), d for decimal (there is no default, it must be specified), and h for hex.
<schlick>
d for decimal (there is no default, it must be specified), and h for hex.
<kmagdsick>
because often some interns will just copy some formulas out of some books
<kmagdsick>
and get things all wrong
<schlick>
I'm not sure if octal is worth including. I've often wondered why it's used anywhere.
<schlick>
I'd be interested in feedback on that.
<schlick>
Hex would have to be all caps, the suffix is always lowercase.
<kmagdsick>
yea, I'm a big fan of \x
<kmagdsick>
\xFF
<kmagdsick>
\xCA\xFE\xBA\xBE
<schlick>
Then you think not having the wierd C numeric syntax is bad?
<kmagdsick>
I really like Erlang's numeric literals syntax
<kmagdsick>
16#FF == 10#255 == 2#11111111
<kmagdsick>
base#value
<kmagdsick>
2 <= base <= 36
<schlick>
That'd be ok.
<schlick>
Though I can't think of a lagitimate use for anything but 2, 8, 10, and 16.
<schlick>
And 8 is iffy.
<schlick>
I guess so long as people are used to specifying ASCII that way base 8 will be in use.
<kmagdsick>
schlick: but there may be a legit use, and it's no extra code required to get the extra fuctionality
<kmagdsick>
schlick: so you might as well allow base 2 to 36
<kmagdsick>
SHA1 URNs are sometimes defined in base32
<schlick>
I suppose. I just have concerns for readability.
<kmagdsick>
although, a different base32 than that used by Erlang
<kmagdsick>
A-Z2-9 instead of 0-9A-W
<schlick>
Erlang uses the latter?
<kmagdsick>
yes
<kmagdsick>
err A-V
<kmagdsick>
so 0 is always 0
<schlick>
It seems far more sensable. It's consistent with how hex is handled.