cmrx64

24 ms·

301.
by cmrx64 8y ago
not coq but HOL4 and Poly/ML. there are verified HOL kernels but you’d need to do substantial manual validation of the exported theorems to make sure they didn’t get subverted during proof export.
302.
by cmrx64 8y ago
You might enjoy this, which I wrote a few years ago. The project is dead now. https://robigalia.org/blog_drafts/2016/12/23/what-time-is-it...
303.
by cmrx64 8y ago
Vaguely related but check out http://ceqea.sourceforge.net/ , paper: https://arxiv.org/abs/1811.02478
304.
by cmrx64 8y ago
http://iabak.archiveteam.org/
305.
by cmrx64 8y ago
I paid over USD 20/pack for cigarettes while I was working in Sydney. That alone forced me to cut my intake substantially. vs the ~5.75 I spent per pack in NH.
306.
by cmrx64 8y ago
Not HDMI, apparently. https://gizmodo.com/363154/audiophile-deathmatch-monster-cab...
307.
by cmrx64 8y ago
I’ve known about this for a few years. Someone brought it up pretty early in cargo’s development. Interesting to see it used in the automotive space: https://uptane.github.io/
308.
A framework for securing software update systems(theupdateframework.github.io)
4 points by cmrx64 8y ago|1 comments
309.
by cmrx64 8y ago
This book is a real joy to read. I got to peek at a draft at OPLSS 2017 and have been waiting impatiently for it to come out. The detailed, carefully worked examples one after another that this style of book is famous for is adapted beautif
310.
by cmrx64 8y ago
it’s a pretty standard type theory lambda calculus, written as sexps because it’s inside racket, but it’s its own thing.
311.
by cmrx64 8y ago
http://www.ghielectronics.com/products/ucm
312.
by cmrx64 8y ago
> The MMU was only recently standardized so I'm not sure if it's actually implemented in any hardware or software yet, but once you have those two things it should be fairly straightforward Chips with MMUs have been taped out f
313.
by cmrx64 8y ago
As another vanilla anki user, what are your favorites?
314.
by cmrx64 8y ago
yes. https://groups.google.com/a/groups.riscv.org/d/msg/isa-dev/e... has a long thread about this. it's not the worst thing in the world, but I think the choice is confusing when it seems easy
315.
by cmrx64 8y ago
rv32 and rv64 are incompatible. this is unfortunate, and it's not clear to me what the tradeoff for that is.
316.
by cmrx64 8y ago
These fully homomorphic encryption systems can do boolean circuits, which are no more powerful than the arithmetic circuits you get with zk-SNARKs (in fact, are an instance of arithmetic circuits). And with some zk-SNARKs, you get recursive
317.
by cmrx64 8y ago
Luqman got some neat results getting this to work iirc, way back in 2014.
318.
by cmrx64 8y ago
I added support for loading plugins to the pass manager because I could. It was never really useful. I had a vision for rustdoc_ng, which was that it would do all the dirty work of collecting information from the (complex) Rust AST into a (
319.
by cmrx64 8y ago
previous discussion https://news.ycombinator.com/item?id=9887548 https://news.ycombinator.com/item?id=8590816 https://news.ycombinator.com/item?id=11836520 https://news.ycombinat
320.
by cmrx64 8y ago
It's extremely easy to wire up a USB-C connector to any legacy USB controller, at least by my reading of the relevant specs. https://imgur.com/a/tL5lDZ5 is what you need logically (I think).
321.
by cmrx64 9y ago
Seems you discovered mindfulness :). "eventually I learned to catch myself whenever I was seeking this form of comfort" is the hard part that a lot of people don't figure out on their own. go you! https://en.wikipe
322.
by cmrx64 9y ago
this is pretty lame. ok, it’s nice that you reject it. so what? who cares? this is the same sort of grandstanding in my eyes.
323.
by cmrx64 9y ago
the "buy it for life" subreddit helps a lot here, for at least narrowing down the search space.
324.
by cmrx64 9y ago
have you watched KEDi? :)
325.
by cmrx64 9y ago
Implying management isn’t tech? You mean isn’t engineering? (Well, people engineering....)
326.
by cmrx64 9y ago
See, once you have a spec, you have TWO jobs. Verification, showing that the spec and the impl agree. This is usually done with comprehensive tests if it's done at all, and very rarely with formal methods (since formal specs are so rar
327.
by cmrx64 9y ago
Yes. https://microkerneldude.wordpress.com/2016/06/16/verified-so...
328.
by cmrx64 9y ago
metis is a first-order automated theorem prover. the metis tactic will handle encoding the goal as a first-order problem, using ~just the rules you provide it, invoking actual-metis, and reconstructing a proof (in the kernel logic) from the
329.
by cmrx64 9y ago
People like to tout this idea about a lot, but I've never seen it used in any rigorous way. It's SUGGESTIVE of program behavior, but I haven't seen any tools for (attempted) extraction of even just FSMs from basic type-level
330.
by cmrx64 9y ago
no. if you're going to go through the trouble to do that, just fix your bullshit broken fucking password requirements.

More ›