wucke13

I pay 0% capital gain tax and use a broker with nearly 0 fees which allows me to rotate for free (almost)

How so?

Software distribution for Linux can be hard. Many distros, different conventions, no FHS is long forgotten, ...

However, Xilinx Vivado and Vitis are so obtusely distributed, making it incredibly hard to package them well.

Three random issues I remember:

1. We had a lot of trouble with Vivado projects randomly breaking. The culprit: German localization combined with automatic clock frequency derivation. Depending on which logic blocks where wired up how, you would get i.e. 99.999 MHz instead of 100 MHz. Apparently, Vivado uses a localized printf (or equivalent) to generate TCL scripts. In German localization, the decimal is a comma, which is interpreted as additional argument in the TCL scripts. 2. For simulation, scripts scripts are copied from a template folder to the user folder, and subsequently adjusted. They are copied in archive mode. If the template is read-only to the current user, so is the new copy, thus failing the subsequent adjustment. 3. If you run the installer with --help as argument, it pops up an X window displaying the help. In general, IIRC, we need to run a headless X just to run the installer in CLI/batch mode.

From a Linux distro maintainer perspective, the packaging is horrible. In particular separation of base installation, configuration, and add-ons is non-existent. Large amount of vendored dependencies, only then to depend on the most minute little packages that Ubuntu supposedly ships.

Setting up a reliable, reproducible CI/CD environment based on Vivado is a large headache.

That all goes to say: if anything, AMD/Xilinx should be paying its customers to deal with this. Unless there is a major improvement in the software distribution practices for Linux, I could not justify to my employer paying money for this experience.

On the other hand, if they commercialize on Linux support, there is soooo much that they can improve by a lot, who knows. Hope dies last and all.

My take: containers forced devepopers to declare various aspects of the application in a standardized, opinioated way:

- Persistant state? Must declare a volume. - IO with external services? Must declare the ports (and maybe addresses). - Configurable parameters? Must declare some env variables. - Trasitive dependecies? Must declare them, but using a mechanism of your choosing (e.g. via the package manager of your base image distro).

Separation of state (as in persistency) and application (as in binaries, assets) makes updates easy. Backups also.

Having most all IO visible and explicit simplifies operation and integration.

And a single, (too?!?) simple config mechanism increases reusability, by enabling e.g. lightweight tailoring of generic application service containers (such as mariadb).

Together this bunch of forced, yet leaky abstractions is just good enough to foster immense reuse & composability on to a plethora of applications, all while allowing to treat them almost entirely like blackboxes. IMHO that is why OCI containers became this big, compared to other virtualization and (application-) cuntainer technologies.

For the seL4 proofs a subset of C was formalized, for example.

(Already mentioned) CakeML would be another example, together maybe with its Pancake sibling.

Also: WebAssembly!

That's pohibitively expensive in the general case when external input is used and/or when arithmetic is used on the values (main differerence to sum-types).

I know quite some people in the safety/aviation domain that kind of dislike the subranges, as it inserts run-time checks that are not easily traceable to source code, thus escaping the trifecta of requirements/tests/source-code (which all must be traceable/covered by each other).

Weirdly, when going through the higher assurance levels in aviation, defensive programming becomes more costly, because it complicates the satisfaction of assurance objectives. SQLite (whiches test suite reaches MC/DC coverage which is the most rigorous coverage criterion asked in aviation) has a nice paragraph on the friction between MC/DC and defensive programming:

https://www.sqlite.org/testing.html#tension_between_fuzz_tes...

Neither the Rust nor the Ada spec is formal, in the sense of consumable by a theorem prover. AFAIK for Ada Spark, there is of course assumptions on the language semantics built-in to Spark, but: these are nowhere coherently written down in a truly formal (as in machine-readable) spec.

I think what parent was about is open vs. closed loop control, not fly-by-wire or not. Both their and your point stand of course.

I have dedicated a large chunk of my (arguably short) professional career on improving upon this, mostly in the safety critical software domain. What was your experience back then, what made you leave ultimately, and what do you do now?

Rust in particular with miri is quite impressive at catching them. You just run your testcases via

    cargo miri run

It doesn't necessarily, but it can. Genode/SculptOS is kind of a microkernel OS framework, and it can use seL4 as the kernel.

Here is a talk about that porting effort:

https://m.youtube.com/watch?v=N624i4X1UDw

Gernot Heiser would strongly disagree with you on the last one :D

I'm not so sure, I thought "patch" originated from hole punching cards to program stuff. A software patch was literally a patch of tape that hides an errorneously punched hole in such a card.

The term patch-cable seems to be way younger.

https://www.pe0sat.vgnet.nl/sdr/iq-data-explained/

This is an excellent introduction to the concept and also to the why complex numbers are used to represent signal samples.

Is this in effect introducing algebraic effects by concept? E.g. the io passed in is an effect handler, and it is the effect handler's choice whether to perform stack switching (or other means of non-blocking waiting) to enable asynchronicity?

This seems to go into a similar direction like ZeroTier, but actually open source. There is almost no discussion of this in the western hemisphere, but I'd be interested what people think about it.

When I first read the examples, besides my laughter, I felt a similar disconnect im the semantics of the chosen German words. Thank you for you suggestions, I agree with all of them, they are better indeed IMHO.

I think ZMK (available on the Nice!Nano) does exactly that already?

Would the Paris Climate Agreement not qualify as a treaty?

Tangentially relevant: Gernots list of benchmarking crimes.

https://gernot-heiser.org/benchmarking-crimes.html

you can pass integers and pointers around

No, not even that (the second thing, passing pointers)! WASM has a different address space (starting from 0), effectively indexing into the WASM module's linear memory. A pointer/reference from the outside env can not be dereferenced from within the WASM bytecode.

The multiple linear memory proposal can circumvent this (allowing you to build something somewhat similar to a simple MMU/address translation engine), but language support for that feature is sparse (AFAIK, Rust does not expose any way to access a different than the default linear memory for example).

There is various hacks around it, but sharing memory block-wise between WASM and outside env is involved already.

Note to self and others: please don't plug in/out a TRRS into your keyboard while it's powered. The TRRS usually shortens pins during insertion/removal, which can damage your keyboard. Most keyboard designs do not properly guard the circuitry against the evil of TRRS.

As in?

The nixpkgs have a rather elegant way to deal with that. Let's presume you need a libpng for an armv7 platform, such as an old RaspberryPi. Then Nix allows you to

- get a suitable cross compiler toolchain

- pick whether you want dynamic or static linking (most likely static when the target system does not come with /nix/store)

- compile all prerequisites for the library such as transitive dependencies

- compile the library with the cross compiler for the selected target arch

All in one command line call, that does not require you to 'apt-get install' any of the tools manually:

  nix-build '<nixpkgs>' -A pkgsStatic.libpng --arg crossSystem '{ config = "armv7a-unknown-linux-gnueabihf"; }'

For a local databus it has been relatively unimportant. However, there are radio data links in/out of the aircraft. The scope of data for these links is quite limited today, but likely to grow significantly in the future. There cryptographic properties become important, and a currently missing. An example would be ACARS.

Also in some aircraft types these data buses are unfortunately not so very hard to access (i.e. accessible from the cabin, with undetected access being even plausible in some cases). So some resilience might not hurt in these cases.

It's important that failure of critical systems is far less threatening than systems providing plausible, yet incorrect data. Redundancy and monitoring catches most of the former but not the latter.

The observation that ARINC 429 can be tapped, and that an active wiretap can alter data on the bus is of little surprise. The technological challenge is not high, the bus is comparable to a serialport at ~115200 baud. Considering that the technology surfaced in the 1970s, it is of no surprise that physical access restriction is the only means of security.

More interesting IMHO would be what can be done to accelerate the adoption of new technologies (especially w/r/t cryptography) in avionics. This is more than anything a cultural problem; How to convince regulative bodies, how to satisfy processes, how to re-balance the proven-in-use argument (where stuff gets more favorable safety assessments when it has been used long enough) vs crypto-agility (where the same thing from today just tomorrow becomes insecure without changing itself, because of some external discovery).

The technology is there, but the aviation community is not yet. Another nice read in this domain is "Economy Class Crypto: Exploring Weak Cipher: Usage in Avionic Communications via ACARS"[1, 2]. I only say mono-alphabetic substitution cipher.

An interesting connection of Blockchain-tech, safety and security can be found in "Verifiable Computing in Avionics for Assuring Computer-Integrity without Replication" [3]. Here the authors leverages zero-knowledge proofs to prove to a downstream actuator that its commands are indeed correct results yielded by the application of the appropriate control law on the provided sensor inputs. However, this work is probably at least a decade away from being applicable in actual certified aircraft.

[1] https://link.springer.com/chapter/10.1007/978-3-319-70972-7_... [2] https://www.cs.ox.ac.uk/files/9693/fc-paper.pdf [3] https://publ.sec.uni-stuttgart.de/reinhartluettighuberliedtk...

Which almost reads as a cautionary tale about mechanisms like Dust's `unsafe`. Not necessarily the specifics of the Rust, but the overall idea of having a safe (by whatever means) sunset of operations and and additional unsafe operations, which eases code analysis tremendously. You can't got without unsafe in most embedded systems. But it's good to very explicitly mark in the code wherever the unknown depths of UB lurk if not the most attention is exercised.

Asbestos is super inert, which made it a very nice material for many applications. However, mechanical interactions of small particles with cellular matter can still cause health issues if I understand correctly. And this is, what the whole fuzz of micro plastics is about, not? Even without biological/chemical reaction, if particle size is small enough, ...

One of the people involved works for the MPI as a crypto researcher, however the project itself was funded by NLnet