spaintech

While both TLA+ and ADA/Spark might be necessary, I haven’t noticed much mention of ADA/SPARK here, which kind of surprised me that they are not used in conjunction as frequent as I might have thought.

For some critical software we developed, we used TLA+ for high-level formal specification. As mentioned earlier, transitioning the actual implementation to another language can be challenging, especially if partial hardware bootstrapping is required. We ended up implementing the high-level specification created in TLA+ using ADA/Spark, which minimized our exposure to buffer and assertion failures. However, optimizing the code to meet performance thresholds was at times frustrating and time-consuming, like any low-level implementation with a new tool/language for us.

I’m curious about any new tools or workflows for leveraging TLA+ high-level specification implementation into other languages like C and Rust. What approaches are people taking once the formalized specification is verified in TLA+ to complete the implementation?

I might be out of the loop, but using TLA+ spec and translate then to other languages hasn’t been a successful use case for LLMs. While they can be helpful, a significant effort is still required to ensure that implementations accurately adhere to the specifications.

I enjoy this article showing up here once in a while. It makes me think about the stack of abstractions we actually live in… CPU -> microcode -> ISA -> firmware/BIOS -> OS + drivers -> C abstract machine -> your app. ( I left our virtualization purposely thinking of a bare metal stack )

Current ISAs have so much machinery underneath that it’s hard to tell when you’re talking to the iron and when you’re talking to the microcode

You can still argue that Forth on a Forth CPU is a genuinely low-level language. :)

You can like the character or not, but there is a trend I’m following ( heavily vested in NVIDIA, so tongue in cheek when I say this ) that might be highly align with Zitron. Looking at the moves from NVIDIA ( Groq )and AMD ( Taalas ) which are pure inference plays. I believe this shows that the impetus to train a better-bigger model might be coming to a level of maturity that might merit a serious threat to the frontier labs.

For frontier labs, their fund-train-new model play might not be as effective, and a shift of spent of compute cost moving away from training to inference might be a tell-tell sign of the LLM as we know it plateauing out as scale is just not as effective. Open models might also be placing a major pressure on meeting then revenue targets need to sustain the model, lots of customer hosting their own inference to mitigate costs.

If you only move the needle just slightly in the direction of inference, frontier labs will soon loose their alphas. Becoming just another SaaS for inference might not be as attractive unless you are Google/MSF ( IMHO ).

Should this pan out, it could be a scenario where the NeoClouds could soon loose their biggest customers, so I tend to agree with that aspect of Zitron’s view.

Thoughts?

It personally feel that Forth if often overlooked as a solution. It’s great for lowlevel embedded work… even on complicated x86 hardware. I also think that people shy away because the tooling is thin and often DIY, but a Forth exokernel plus a single-purpose app can squeeze more from the hardware.

Tethered Forth programming on small devices is an underrated opportunity, IMO. There is also the opportunity to revise the OpenBoot project, I remember the days of automation for deployments at the Bios, it was an amazing tool for massive deployments of Sun T systems in telcos.

Not sure if you are aware of this, but LUNA does this already.

https://www.usenix.org/system/files/atc23-zhu-lingjun.pdf

My take on why Google bought Wiz is pretty straightforward. First off, Wiz brings a rock-solid CRM loaded with all those juicy contracts from the top cloud players. Add to that a proven enterprise team that knows exactly how to sell the product, and whom to sell to. And you’ve got a recipe for success. Every Wiz win is just a possible upsell for GCP; especially when GCP isn’t even the market leader in cloud. IMO, it opens the door to a whole lot of sales opportunities and deep-rooted relationships with top-tier cloud customers. To me, that all points to a pretty hefty price tag on the table

I agree, hence my direct comment of malicious firmware… For me, the open question is, can one still write a malicious firmware on the ESP32 without the non documented opcodes?

First and foremost, I have no affiliation with any of the authors previously mentioned. However, I would like to pose a question to the community:

Is it feasible to exploit these undocumented HCI commands to develop malicious firmware for the ESP32? Such firmware could potentially be designed to respond to over-the-air (OTA) signals, activating these hidden commands to perform unauthorized actions like memory manipulation or device impersonation.

However, considering that deploying malicious firmware already implies a significant level of system compromise, how does this scenario differ from traditional malware attacks targeting x86 architectures to gain low-level access to servers?

If an LLM’s logic is derived primarily from its training phase… essentially, by following patterns it has previously seen; doesn’t that underscore the critical role of training? We invest significantly in reinforcement learning and subsequent processes, so if the paper’s claim is accurate, perhaps we need to explore innovative approaches during the training phase

Correct, I updated the title of the original paper. Thank you your bringing up.

When a language model is trained for chain-of-thought reasoning, particularly on datasets with a limited number of sequence variations, it may end up memorizing predetermined step patterns that seem effective but don’t reflect true logical understanding. Rather than deriving each step logically from the previous ones and the given premises, the model might simply follow a “recipe” it learned from the training data. As a result, this adherence to learned patterns can overshadow genuine logical relationships, causing the model to rely on familiar sequences instead of understanding why one step logically follows from another.

In other words, language models are advanced pattern recognizers that mimic logical reasoning without genuinely understanding the underlying logic.

We might need to shift our focus on the training phase for better performance?

This is a fascinating study, it reveals that ant groups significantly improve their problem-solving abilities through effective cooperation, whereas human groups do not show similar enhancements and can even perform worse when communication is limited. This difference is attributed to ants’ simple cognitive structures, which facilitate seamless collaboration, while humans’ complex cognition leads to variations that hinder efficient group performance. It seems that the advantages of collective cognition depend on the underlying cognitive and cooperative mechanisms of the species… found it a great read.

Dito on the upvote, esthetics are pleasing and I love the transition of the board. Not sure if that was sand or not… but now in hunting for the files… would make a nice gift for a friend that has it all, rated at 2000+ in chest.

Good point, but still, you are leaving the user with too much leverage on the underlying architecture, again from the OS’ perspective.

They way I’m considering this is, one could provide virtual time sources, removing the high resolution timers, where the OS has more of a coarse-grained timer. Not sure the implications, but if needed, one could add jitter or randomness ( Noise ) to the virtual timer values…

This would further prevent thread from running out of sync with the resto of the threads.

Further, one could also add a stack based shared memory model, LIFO would provide a highly predictable behavior from an application perspective. If you make it per process, the shared stack would then be confined to the application. No sure if possible ( haven given deep thought ) but the stacks could be confined to specific cache lines, removing the timing differences caused by cache contention…

When I read these articles, I always ask myself if this is more of a joint OS-ISA issue than just an ISA problem.

Wondering if a well defined OS system, with strict enforcement of memory boundaries at the OS level and at the application level, where the application sits in a well defined deterministic execution model would mitigate some of these unpredictable state transitions.

If one considers a minimalist OS, micro kernel for example, lowering the attack surface, would this not explicitly prevent access to certain microarchitectural states (e.g., by disallowing certain instructions like clflush or speculative paths)? This could be accomplished with a strict memory management jointly at the OS layer and the binary structure of the application… one where the binary has a well defined memory memory boundary. The OS just ensures it is kept with in these limits.

If we consider President Javier Milei’s perspectives on monopolies, as articulated in his address at the World Economic Forum [1], we can apply his reasoning to the case of Starlink’s potential dominance in direct-to-phone satellite connectivity. In his statements, Milei challenges the traditional view that monopolies inherently lead to market inefficiencies. Instead, he assumes that monopolistic positions, when achieved through “innovation” and “without government interference,” can drive significant technological advancements and economic growth.

Applying this to Starlink, its emergence as a leading provider in satellite-based mobile connectivity could be seen as a result of substantial innovation and investment. Such a position enables the company to offer services that were previously unavailable or limited, particularly in underserved regions. Considering Milei’s argument suggests that in the absence of government-imposed barriers, a monopoly like Starlink’s can maintain competitive pricing to deter potential competitors, ensuring consumers benefit from both advanced technology and reasonable costs.

Milei emphasizes that market failures are often the result of state intervention rather than the natural outcome of market dynamics. In the case of Starlink, minimal regulatory interference could allow the company to operate efficiently, maintaining an environment where innovation thrives, and consumers receive enhanced services. Its the potential drive of the market (competitors) and innovation to keeps them in check with pricing and perceived consumer value. [2] [3]

[1] https://www.hoover.org/news/market-ourselves-argentine-presi...

[2] https://www.weforum.org/stories/2024/01/special-address-by-j...

[3] https://lexfridman.com/javier-milei-transcript/

Forthic is a stack-based programming language developed by LinkedIn to enhance the flexibility and tweakability of applications. By embedding a Forthic interpreter into an application, developers can allow end-users to modify and extend the application’s behavior at runtime. This approach has been utilized by LinkedIn to build numerous internal tools, particularly those based on Jira for program management.

The Forthic repository on GitHub offers two primary interpreters:

1. Python-based Interpreter: Designed to run within a Flask application, enabling the creation of APIs that can be revised at runtime.

2. React-based Interpreter: Facilitates the creation of user interfaces on-the-fly.

For a comprehensive overview of Forthic, see: https://github.com/linkedin/forthic

Dang, that many startups in that short period of time, how is that plausible? I say that wholeheartedly considering the time it takes to take something from an idea to a PoC to an MVP. Don’t get me wrong, I know there are plenty of quick slap together projects out there, similar to the one been commented here, they are more like a marketing wrapper of bundles from others people’s work, which is something to be frowned upon… specially if you are technically motivated.

Well, IMHO, when considering a project, knowing that you are solving for a customer demand problem is very different than from a VC minded problem. I personally would never advise or be part of such an “Arrangement.” These are my clear principles, and my success will come or fail, but my integrity will never be questioned.

Been following this development here for some time… many threads already provide for some great comments on the idea.

I find it both interesting and exciting to see a new os for the could era. I do feel like the DBOS is still not singular, PICK ( already mentioned) but also mentioned in other thread where Taurus OS and the Plant 9 project, which also leverages a database on a file system as a core for system resource management.

In my own thinking of a cloud OS, and particularly considering the focus on server-less applications as mentioned in the article, I have been inspired by Forth’s Dictionary data structure as a lightweight data structure concept where the core state and application contexts are managed through modular dictionaries, each with isolated and secure contexts. OS has a Core Dictiory, and each application is contained with in it’s own namespace dictionary… ect.

Message passing between applications could be efficiently handled using a tagging/queue system, potentially extending to RDMA for distributed environments. This could offer a lightweight, performance-optimized alternative current OS options, particularly in resource-constrained or highly distributed systems for server-less infrastructures.

This is great news for those invested in ARM CPUs. I, for one, purchased a Lenovo X13s when it first came out for around 1,900 EUR. Unfortunately, my experience with it on Windows was subpar, and it was even worse on Linux. At the same time, I bought my wife a MacBook Air (not sure if it was an M1 or M2), and it was snappy and very pleasant to use. I bought the Lenovo based on the hype from benchmarks, and it seemed like a capable system initially. However, I couldn't tolerate all its limitations and ended up returning it, as it performed no better than a Chromebook I had bought earlier.

I'm hopeful that Snapdragon will offer an alternative ARM platform for laptops that can handle more than just browsing. As consumers, we need options, and the more, the merrier. I'm still undecided about the short-term success of Snapdragon. For now, I'm betting/waiting on the MacBook Air with an M4 as my daily driver, although I do prefer the Lenovo ThinkPad format.

Wow, I thought the article was recent and thought there was a second release.

I’d like to congratulate the author, this is not only a great source of technical depth in the real of languages, but also a great read as far as the layout and the small details in the graphics made is a source that I just keeps me engaged in the reading. I’s one of those books that feels will be relevant for many-many-years to come!

Congrats and thank you!

Why so, the goal was just to post my original comments, I was messing around with the python to do this and I missed the error. My sole purpose is to just have the agent do my task, not take over my comments. Hence both my own comment and the AI extension of my intended post. Just like this one FWIW. >:D

I don’t know micropython enough.

I know that it is substantially supported on the ESP32, which is great, but I’m not sure if it’s able to give you the HW access that Forth has, you can extend and build your own drivers on the Forth system, which is my main use case. I like to do things as bare to the metal as possible and C and forth give me that, it’s the same reason I never used the arduino framework.

Was trying an autopost agent I’m trying to build, still not working… >:D

Fantastic, love the writing style and the graphics! Simple, compact, and useful.

Your comment “Fantastic, love the writing style and the graphics! Simple, compact, and useful.” reflects an appreciation for the article's clarity and visual appeal. To extend this, you might consider highlighting specific elements that stood out to you. For example:

I particularly admired the way complex technical concepts, like the Platform-Level Interrupt Controller and UART Interrupts, were explained in a straightforward manner.

(I wish I could hand draw that well. :) )

The graphics played a crucial role in demystifying the intricacies of RISC-V Interrupts and the initialization process in the BL808 SoC.

It's impressive how the article managed to make such dense material accessible and engaging, especially the sections on enabling interrupts and handling them through the PLIC.

The troubleshooting part, detailing the unexpected behavior with interrupt priority, was especially useful, I have been bitten by that very essence in UART dev.

I recommend the article, it serves as an excellent resource for anyone delving into RISC-V architecture or embedded systems programming. I think it extends to most UART development actors RISC systems in general. Well done!

I highly recommend using Forth for interactive exploration of hardware. In my opinion, C-Forth and uEForth are particularly well-suited for the ESP32. Even when I choose to develop C-based Baremetal solutions for the ESP32, Forth proves incredibly useful for quickly testing and validating my ideas. This is especially true for verifying physical wiring, as it significantly reduces the time spent troubleshooting potential errors, whether in my own work or when examining a pre-made board.

What a fantastic site! Wish more titea were build this way. It was an awesome experience! I’m an outsider living in Spain for the last 22 years, I think that while the content portrays a reality of the high rise movement in Spain, there is an angle that was missed. It is important to say that the at time draconian land laws pay an important role in the urban landscape. Not to mention that Spain relative young democracy ( we won’t talk about that the today ) also plays am important role into shaping the urban seen. Lots of change in the government parties have also lead to constrains and or retains during several periods. Ok his has mean that different areas would grow artificially dependent on the “favoritism” at play at the moment through favorable zoning changes or subsidized public housing. Albeit and thankfully at the moment, Spain has not discovers property taxes like the US, it contains growth with little planning and driven by massive speculation which has been an economic driver for major cities even with relative low occupation rates. There is also the fundamental culture of buy vs rent that drives for more flats been built to keep up with the demand. On the plus side, one the the biggest differences I have seen in Spain is a relative wide spread economic demographic in the cities, where you don’t see the major changes like most other major city across the world, it happens but it’s neither common or as drastic as the rest.