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).

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

And if your code actually touches UB, mirei will most likely point out exactly where and why.

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.

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?