cmrx64

33 ms·

391.
by cmrx64 10y ago
That makes sense. I wasn't aware of the details, but looking into it now, "onion"/hidden services are a way of establishing tor circuits which are then used normally. Thanks!
392.
by cmrx64 10y ago
I'm curious why they decided on a "special-use domain name" instead of something like "onion://hash".
393.
James Webb Space Telescope Exposure Time Calculator(jwst.etc.stsci.edu)
2 points by cmrx64 10y ago|0 comments
394.
by cmrx64 10y ago
I'm curious how long it took to build their search index, and how they do it/what technologies/algorithms they are using. That's a lot of data!
395.
by cmrx64 10y ago
I'm definitely guilty of this one. My big mistake is I always think "oh this will be an easy fix" when configuring a CI system, and then it doesn't work, and I don't split into a new branch then and there.
396.
by cmrx64 10y ago
Unfortunately I can't take the credit for the (IMO) brilliant name. For over two weeks in ~September 2015 I was wracking my brain for a decent name and one of my fellow students came up with it. Lots of great name-based tie-ins.
397.
by cmrx64 10y ago
Entirely different, but with a *nix compatability environment (not unlike Windows' lxss or Solaris' brands/zones)
398.
by cmrx64 10y ago
The best resource for getting started with Isabelle/HOL is http://www.concrete-semantics.org/ . Freely available.
399.
This Year in Robigalia(robigalia.org)
61 points by cmrx64 10y ago|6 comments
400.
by cmrx64 10y ago
Good timing, I'm putting out the one-year retrospective on Robigalia in just a few minutes :)
401.
by cmrx64 10y ago
I'm not so certain. Fully automated theorem proving in powerful logics like Coq uses is extraordinarily hard and expensive (between "P=NP" and "halting problem" levels of hard and expensive). "Tree search with
402.
by cmrx64 10y ago
Ok, interesting.
403.
by cmrx64 10y ago
I had the same thought. Does the world really need another (presumably) stratum-3 server running in Amazon's cluster, when Amazon already runs a pool of stratum-2 servers? ([0-3].amazon.pool.ntp.org).
404.
by cmrx64 10y ago
In both of the papers I reference, there is a javascript component running on the JWST. Of course the mission planning stuff is all groundside.
405.
by cmrx64 10y ago
One of my friends works at the STSCI on various visualization and simulation tools (all web-based, written in a modern stack!) for planning missions for this thing. It's a really really neat project. The telescope itself is "scrip
406.
Putting the Rust in Trust: A Path to Rust Verification(robigalia.org)
10 points by cmrx64 10y ago|0 comments
407.
by cmrx64 10y ago
I agree. Lots of language make it too hard to use custom equivalence or ordering relations.
408.
by cmrx64 10y ago
Turns out, there are many more interesting equivalence relations on values than simply structural equality!
409.
by cmrx64 10y ago
It'd be neat to see emulators of this quality on the Switch, which looks like it's going to be a fantastic console. OTOH, quite a bit more expensive for the consumer!
410.
by cmrx64 10y ago
Neat! I look forward to seeing what they come up with :) For similar sorts of things, check out NeSy: http://daselab.cs.wright.edu/nesy/NeSy16/
411.
by cmrx64 10y ago
It's currently integrating higher-order logic (HOL) with a reimplementation of HOL Light.
412.
by cmrx64 10y ago
Seriously. With a simple genetic algorithm you can do significantly better. Considering 2-grams etc. It's nice that they decided to write up what they "learned" with this simple experiment, but they didn't try very har
413.
by cmrx64 10y ago
And it integrates many "vimisms" via evil-mode. I'd been a vim user for a long time but was increasingly dissatisfied as I got deeper into extending it. I've found the opposite of emacs (especially with spacemacs) almost
414.
by cmrx64 10y ago
spacemacs ;)
415.
by cmrx64 10y ago
I use let's encrypt for gitlab pages, as seen here: https://robigalia.org/ The key is doing a dns-01 challenge, instead of http-01, so you don't have to put challenge-response garbage in your repo.
416.
by cmrx64 10y ago
> I wonder if one could get funding for an effort like Robigalia to reach production quality and have Servo running on it. Given the feature set of Servo, it's a safe bet that the required features would provide a reasonably complet
417.
by cmrx64 10y ago
I wrote on their forum about why they "shouldn't" use seL4, and definitely shouldn't port it to Rust: https://discourse.redox-os.org/t/why-not-port-sel4-microkern... If the goal is trusthworthy, rel
418.
by cmrx64 10y ago
the master branch of sel4 is always passing verification, for the verified platform: armv7-a on a Sabre Lite. the x86_64 verification is coming out soon according to the roadmap.
419.
by cmrx64 10y ago
Where do you get all that helium?
420.
Epitaph. A text game(mkremins.github.io)
5 points by cmrx64 10y ago|0 comments

More ›