dmytroi

Then it will be too noisy or too slow to be useful due to too many intermediate states. The feature of TLA+ is that it forces you to greatly dumb down the code to be able to use it, so it's more of verifying an algorithm represented as visual graph blocks rather than verifying assembly instructions.

I understand the wish for a magic bullet to just verify already existing code, but I recon the answer to this is to verify code before it's even written.

Same here with v3 and now being flabbergasted that my "open" project is suddenly dead-ended. (Re)doing an alternative software for PCB v3 is definitely possible, it just runs into economics, at average hourly rate we would put into it it just cheaper to buy decent espresso machine and move on.

Some popular in inner city: Tanto strandbad, Långholmsbadet, Smedsuddsbadet, Fredhällsbadet, Kristinebergsbadet, Brunnsviksbadet. Plenty of folks swim during hot periods in summer.

Also ELF segment alignment, which is defaults to 4k.

UE5 dropped support for 32 bit platforms, so at the moment not without some code changes.

WebAssembly is working on adding support for 64 bit address space though.

Mostly integration, for example some library can only be configured via env variables, but a developer might want to configure it from with-in the app it's integrated into and used from.

Also, few weeks ago I found a use for them when trying to pass configuration from Java/Kotlin to C++ library to be used during static constructors (invoked during dlopen) on Android, because at that phase native code cannot call back to JVM.

100% agree for "read only" software, like scanning, diagnostics, etc.

Control software is much more involved topic, let me illustrate it with a scenario: one family member is non-techy but has an insulin pump, another family member is techy and likes to hack around, they made a change to the insulin pump software to "improve it", but by accident the change triggered insulin overdose at night during sleep and family member died. We have rules and regulations not just to have rules and regulations, we have rules and regulations because they are written in blood.

While advocating for ability to freely modifying any life dependant control software is a noble goal, in my opinion it's the wrong end to approach it, instead it would be more constructive if we as computer science industry figure out ways how to make software such as we don't kill people, how to "certify" it in self service fashion (validation passed == no-one will die), etc, it's no trivial and it feels this particular part of our industry is not as developed/main stream as compared to something like civil engineering. If we have easy ways to ensure that modifying software will not lead to death then it will be easier to change the legislation to enforce this freedom.

AFAIK Android updates are not as fast as they could be due to need for mobile operators to re-certify every update as the OS blob contains modem firmware. Apple is able to update iOS faster because modem firmware is separate from the rest of iOS. Hence having open source drivers in the kernel will not improve the situation much.

WASM itself is likely to be successful in some niches, the industry has a know-how for bytecode VM's and integration with LLVM will make it stick for a long while. My bet are computation kernels for web, and porting whole native apps to web browsers via emscripten.

WASI is probably doomed to fail, so far it was proven to be challenging to make "write once run everywhere" API, for example it's difficult to abstract over epoll vs IOCP vs io_uring without reinventing libuv, but making a standard out of libuv API will make adopting any platform changes too slow, because of losing control over the implementation of the API. Having a single standard implementation where the industry is collaborating might be a better way, similar to how .NET is an abstraction over platform API.

Self recursion is not solvable if assuming stack is unlimited, which is never a case in reality. Stack on real computers is usually limited to a fixed size (100-1000kb). Another way to look at it, take all possible bits on a real computer, so all of RAM, all of storage, etc and then iterate over all possible values of it, it will be 2^bits possible values, sure it's a large value but it's still bounded. So it's possible to iterate over all possible states of any program on bounded computer in a bounded time. Hence why it's possible to decide if any program halts on any real computer in bounded time.

Sure one can say input is coming from a network stream then what? For practical issues then we can limit input size to N bits ... For theoretical issues we can discuss if there is a difference between halting or waiting for more input :)

Let's take the _complete_ program state (input, output, RAM, program counter, stack, registers, rand gen entropy source state, etc) and for every possible such state make a node in a graph. Then when we execute a given program for a given state, we get one edge to the next program state node. Then deciding if program halts or not is answering a question if graph has a node with no outgoing edges. It's also possible to build such graphs for programs that never halt. That's the basic idea behind TLA+.

So it's definitely possible to decide halt problem for a bounded computer (any physical computer), it's just not practical in most cases, e.g. amount of memory needed to store graph of all states be bigger than amount of matter in the universe, etc.