touisteur

And yet the automation we pour trillions in, is the one that will do anything, including everything I find interesting and will never clean my own house.

Haven't seen much about SPARK and why3 recently, combined with frontier LLMs. It would seem easier to progressively prove properties from an actual implementation (going from absence of runtime errors to partial functional proof to full functional proof if you can beau the cost) and only focus the Lean effort on places where why3 (and its menagerie) of SMT provers give up ?

It would also seem highly agent-able since verification is very modular in SPARK.

If your soul can bounce back, finding ways your previous research might help, or combine with the breakthrough (or not !) can help. I've used many previous formal/analytic SOTA algorithms and methods for dataset tagging automation, or as feedback for RL, or to speed-up post-training.

You might want to read Dan Simmons' Ilium and if you can stomach some weird post-9/11 shit, Olympos. One of the overarching themes is what you describe... or similar.

Might be a very good occasion to actually improve the test suites from our load-bearing software projects. I feel this will be the decade of a cat and mouse game between LLM PRs and finding good (as in convincing whomever is paying you and is waiting for any occasion to fire you for being anti-progress or something).

Hopefully we get: actual formal coding rules, spec rules, design rules, contribution rules, documentation and testing rules. High Integrity development processes impose that you write all this before you start and makes sure you follow your own rules.

So. I guess... welcome everyone to explicit software and systems development processes.

I have a similar relationship with wireshark. I understand the use of a live capture and display and the attraction of the click GUI.

But at some point I just figured I was wasting so much time in there. Switched tshark and jq or good old bash/awk/grep and gnuplot, back to the command-line, then python for batteries, still using the output of tshark... and then ended writing a pcap(and ng) parser with ethernet-ip-udp/tcp and a full java IDE and never went back. I went the same meandering path with every data capture and exploration tool I had to use repeatedly.

I feel I'm not the only one having this repeated sequence of tooling improvement, hopefully there is a well named scale to describe it.

In the case of the Quantas A380 departing from Changi some shrapnel from the engine explosion did go through the aircraft's body, cutting cables, making a mess of the control-command systems. I don't know how one could contain the kind of energy imparted to these metal bits, especially on engines with so much power...

Keep exploring and writing (please ?) ! Love seeing people explore ... even after Fabrice Bellard had a go at it.

Very interesting work on microvms there. I would add that removing any kind of storage or file-system interaction is reachable for even faster bringup and removing the risk of attacks needing some form of persistence.

Also replacing network access with af-vsock is actually interesting if you want to simplify bring-up. SSH does some magic with vsocks these days too.

SPARK does static analysis (proof) of Absence of Runtime Errors (AoRTE).

As with all things mathworks, migrating away from simulink to alternatives isn't an easy ride. Just having an alternative to Embedded Coder to generate code in another (safer) language proved just too much years ago...

Bright stars are so bright they literally mask areas of the sky. You'll probably need deconvolution algorithms (CLEAN being the standard some time ago, don't know whether some AI/deep-inv approach works nowadays...) to remove them.

Forgot about ONU ! Now I need to look into what an ONU can do, and what one can run on it...

That was a very eye-opening post, full of very interesting details on how modern wired networks work, between NIC and the physical layer... so many mysteries about SFP black magic just falled into place in my head...

Some things that Meta shares or opensources is discrete but amazing. lz4 and zstd and Yann Collet's work. io_uring (don't know if Jens Axboe is still there). And the open timecard projects, and overall OCP work.

I'm not harping on the usefulness. More like trying to understand what would be the merit or use-case of frequent or permanent monitoring of this. Are there know failure/degradation modes from the storage HW or the filesystem, or database problems that would be detected by running this continuously. Sibling answer talks about SAN, which makes sense. Wondering what the other use-cases are here.

Otherwise, yes, of course,using it as calibration after any HW change would be interesting.

Oh thanks. Forgot about this case.

Genuinely curious: where would one expect the drive performance to fluctuate? Wear ? Lack of TRIM ? Some form of timely GC process on disk firmware ? Fragmentation or compaction of some sort ? Maybe weird shenanigans with RAID setups with disks from different vendors and batches ?

Embarking right now on a long-term embedded storage project and wondering what people actually monitor (apart from SMART and latency/throughput at app or db-level).

There's a layer above that, when CLI and bash and sed and tshark are becoming too hairy or slow, and it's 'just' parsing the pcap frames in your language of productivity. Over the years I've built layer over layer of optimized Java code to parse and analyze pcap/pcapng files with either visitor patterns or active iterations (and multi-pass analyses through indexation, or just interfacing with duckdb for months-long-capture analysis to surface low signal-to-noise-ratio events). It builds a good understanding of all the layers and brings the power of a full-featured workbench (language, IDE, libraries, visualization options...).

Built it in Java, and rebuilt it in Ada, and Rust. I find it's a good exercise to learn about a programming language... bonus point, once I have a parser, plugging it live behind libpcap, dpdk, xdp, or just raw sockets is easy.

Aaaaaaand torch is not a simple easy target. You don't just want support but high-performance optimized support on a pretty-complex moving target... maybe better/easier than CUDA but not that much it seems.

But what would they use before bringing in postgis ? I'm curious about the alternatives. MongoDB for example doesn't seem to have a geospatial ecosystem, apart from basic 2d features. Clickhouse ?

BTW if you're interested in the concept of upgrading a sensor without retooling the RF part, and the impact of 'just' putting new COTS racked server hardware and engineering man-hours to get a 'new' sensor with new capabilities, have a look at Julien Plante's work on NenuFAR (which isn't like the SKA at all :-) : https://cnrs.hal.science/USN/obspm-04273804v1 . Damien Gratadour, his PhD supervisor is an amazing technologist, dedicated to improving astronomy instruments, and I was very lucky to work with him and his team... the things the French can string together with small teams and thin budgets...

Forking Firefox whenever the rug is pulled seems doable (with elbow grease), and in the meantime Europeans can invest on problems that don't have an already mature fully open-source solution.

I think Bourbaki did brought forth a shift (clean-up) in mathematical notation and writing, at least in France.

Not to ask anyone for free work but any write-up on this, I'd love to read.

Remembering now that SKA is many, many things and I was talking of the higher-bands array still being installed, but many infos on the -low and -mid arrays are available, for example https://www.skao.int/sites/default/files/documents/Year_In_T...

Sorry, not sure I follow from what I said (explaining how much data sensors produce) to 'increasing the sampling frequency' ? You're usually sampling at larger width to then put specifically taylored pass-band filter and removing aliasing effects and then downsampling. This is a classic signal acquisition pattern : https://dsp.stackexchange.com/questions/63359/obtain-i-q-com...

I think they preserve timestamped I,Q data. Know some people looking at down-sampling, preselecting those signals for longer term storage and deeper reprocessing and they seem to have a 24h window to 'analyze and keep what you need'.

We're still in technological phase where ADCs are far more advanced than storage and online processing systems, which means throwing away a lot. But I have high hopes for a system where you upgrade computing, network, storage (and maybe ADCs...) and you get an improved sensor. Throw man-hours at some GPU kernel developers and you get new science. The limit seems more now about enough people and compute to fully exploit the data than technological...

On SKA from what I understand they're sampling broadband but quickly beamform and downsample as the datarates would be unsustainable to store over the whole array.

Every sensor in the array is sampling at frequency, so - first order - you can use that sampling frequency and the sample size, you get an idea of the input bandwidth in bytes/second. There are of course bandwidth reduction steps (filtering, downsampling, beamforming)...