Viewing profile — 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…

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…

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…

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 …

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,…

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…

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.yo…

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 s…

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…

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 peopl…

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 the…

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 …

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 keybo…

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 …