1,800 karma · joined October 24, 2009
https://linkedin.com/in/synack
I'd love to know more about this. Is it Paxos or something else?
Native Transfer Speed: Up to 400MB/s
21 hours to write a full tape
I’m curious how FreeBSD performs on the same test.
I found the Learning Artsey book from Discord helpful and managed to get up to 15 WPM in about a week with regular practice. Still quite tedious for coding, but good enough for emails and IRC.
https://www.adafruit.com/product/5128
https://github.com/JeremyGrosser/qmk_firmware/tree/artsey_ma...
https://raw.githubusercontent.com/artseyio/artsey/main/layou...
Augeas [1] does a decent job of translating various formats into a common AST which you can edit and write back out, but setting this up is often more trouble than just editing/templating whatever config and moving on with your life.
Many new projects go straight for YAML/TOML/JSON/INI as they're widely understood and relatively easy to parse. I think this is as close to standardization as you'll get.
OpenBSD's developers have gone in the other direction, defining domain specific configuration languages for each of their daemons. They're all different, but they look similar enough that it feels like a cohesive system. You can look at the yacc grammar and see how httpd's config [2] got started as a fork of relayd [3].
[2] https://github.com/openbsd/src/blob/master/usr.sbin/httpd/pa...
[3] https://github.com/openbsd/src/blob/master/usr.sbin/relayd/p...
http://www.faqs.org/faqs/csh-coke-machine-info/
https://github.blog/news-insights/the-internet-coke-machine-...
Looks like it got the Rust treatment a few years ago: https://github.com/ComputerScienceHouse/bubbler
Now if your vectors are INT8/FP8 you’re supposed to shovel them into this accelerator via PCIe, rather than packing into registers for AVX512.
I wish they’d just pick an interface for vector ops and stick with it.
https://web.archive.org/web/20080405212335/http://webmonkey....
It's like using a calculator for your math homework. You still need to understand the concepts, but the details can be offloaded to a machine. I think the difference is that the calculator is always correct, whereas ChatGPT... not so much.
You can find more information in the users guide. https://docs.adacore.com/spark2014-docs/html/ug/index.html
Proof levels depend on your goals, but most requirements are satisfied by proof of “Absence of Runtime Exceptions” (AoRTE), which is easier than a full formal proof.