<civodul>there are lots of things to dislike about the web, but at least it allows language people to pursue interesting work
<philed>civodul: That's got my curiosity. What do you dislike about the web? (not saying I don't have plenty of my own dislikes :) )
<philed>Svetlana: We've had the audacity to invent another scripting language, this one supposedly tailored to theorem proving. Personally, I wanted to just go with scheme and some choice macros.
<Svetlana>trust me, learning new languages is hard and the idea to have all software scriptable in a single language has solid ground
<Svetlana>I'm raging at a lot of software that's not only not scriptable properly, but is scriptable in js (clientside) and in php (serverside) which forces me to learn 2 languages to actually do a single thing
<Svetlana>On the plus side, both the 'frontend' and the 'backend' would be on the user's computer, which makes things a bit easier. But having to keep learning is pretty hard.
<philed>civodul: Otherwise, we're hoping that theorem proving is a unique point in the space of collaboration. You can state the problems you need solved unambiguously, and you don't have to human-check the solutions. The theorem prover is going to be a single indefinitely running runtime, and we hope that'll give us great opportunities to distribute problems and reintegrate solutions.
<civodul>ISTR that jgay was on this channel at some point?
<philed>civodul: On that front, I think we're largely innocent. We want the web to leverage distributed computing power and gather data for recommender systems to help advise users how to solve their problem, and to provide a single stable runtime for people to work in. In theorem proving, with, say, HOL Light, you can be running the same REPL for weeks and just incrementally adding to it. We want a single REPL shared by all users. But the
<philed>whole thing will be open source too, to run intranets for small theorem proving groups.
<civodul>philed: sharing theorem proving experience like this sounds cool, indeed
<DusXMT>I wonder, what for email is available on GNU? Any recommendations?
<jxself>Because Fetchmail+Procmail+Mutt makes for a good combo, IMO.
<mark_weaver>civodul: I've been struggling with hydra. I'm trying to cancel all the jobs in the queue, since it's all for core-updates and that's going to have to be rebuilt from scratch anyway, but my attempts to do so seem to be ignored.
<mark_weaver>also, my last attempt to evaluate core-updates was pending for hours and finally timed out. (just as well, since we have to fix the format warning thing)
<mark_weaver>more generally, I'm rather discouraged by how long it's taking for us to implement security updates to glibc :-(
<mark_weaver>(well, the first time I asked it to clear the queue, it _did_ cancel around 170 jobs or so. but there are many hundreds more that I'd like to cancel but can't seem to)
<DusXMT>I've looked at FPC (The Free Pascal Compiler) as it's on the wishlist, and apparently, it itself is written in pascal, so there needs to be a bootstrapping pascal compiler of some sort before it can be compiled... hmm...
<DusXMT>I personally think the easier route will be to use gpc (GNU Pascal Compiler) instead, but that only works on old versions of gcc (I think up to 4.1)
<DusXMT>It would be interesting to see if gpc can compile fpc, and if that could work, we could build fpc by the gpc compiled compiler, and recompile fpc with that, getting a bootstrap binary which could then be used to build fpc for the user to use... But that assumes gpc can compile fpc, which I kind of doubt it can.
<philed>Get GHC to compile itself to C, first, then you've got a portable GHC?
<mark_weaver>yeah, but that C is not source code. it's not practical to audit it.
<mark_weaver>i.e. the thompson virus would be hidden in that intermediate C code and we wouldn't be able to see it there.
<ijp>(assuming for arguments sake that said virus hasn't bugged the tools you are viewing the source code)
<ijp>the thompson bug is really every paranoid's wet dream :)
<mark_weaver>heh, yeah, it's quite a rabbit hole when you think about it.
<mark_weaver>it would be good to have a bootstrap strategy that doesn't require any previous object code at all, but it would be quite a project.
<mark_weaver>but it practice, it would probably be sufficient to write a very simple C compiler, run it on a very old computer with an old copy of Debian, and use it to bootstrap the last version of GCC that was written in plain C.
<mark_weaver>(crucially, keeping the computer disconnected from the network at all times)
<jxself>Nah, an additional permission thing isn't needed because the modifications to GCC would fall under the GPL's terms already.
<mark_weaver>It's an interesting idea, but I'm not sure what we could gain by investigating this further. If anyone put in a Thompson virus on purpose, I guess that violates laws other than copyright law. If they didn't put it in themselves, but were unwitting users of an infected copy of GCC, then I guess maybe the lack of warranty would protect them to some extent.
<DusXMT>I think I'm going to put that exception I posted abive into my code, just as a fun easter egg
<mark_weaver>I hope you don't put it into any code that might have future importance.