seL4
The-Spiral-Language
seL4 | The-Spiral-Language | |
---|---|---|
60 | 33 | |
4,549 | 907 | |
1.2% | - | |
9.0 | 9.7 | |
4 days ago | 7 days ago | |
C | Python | |
GNU General Public License v3.0 or later | Mozilla Public License 2.0 |
Stars - the number of stars that a project has on GitHub. Growth - month over month growth in stars.
Activity is a relative number indicating how actively a project is being developed. Recent commits have higher weight than older ones.
For example, an activity of 9.0 indicates that a project is amongst the top 10% of the most actively developed projects that we are tracking.
seL4
-
From L3 to seL4 what have we learnt in 20 years of L4 microkernels? [video]
> People like to snob Unix but the fact is: the world runs on Unix.
The world you are aware of runs on it.
> Can we really do that much better or is it just hubris?
Yes. Have a look at seL4[1] and Barrelfish too[2], even though that's no longer active. seL4 in particular is powering a lot of highly secure computing systems. There is a surprisingly large sphere outside of Unix/POSIX.
[1] https://sel4.systems/
[2] https://barrelfish.org/
-
On the Costs of Syscalls
There are also RTOS-capable microkernels such as seL4[0], with few but extremely fast syscalls[1]. Note times are in cycles, not usec.
0. https://sel4.systems/
1. https://sel4.systems/About/Performance/
-
Can the language of proof assistants be used for general purpose programming?
https://sel4.systems
Working on a number of platforms, verified on some. Multicore support is an ongoing effort afaict.
On OS built on this kernel is still subject to some assumptions (like, hardware working correctly, bootloader doing its job, etc). But mostly those assumptions are less of a problem / easier to prove than the properties of a complex software system.
As I understand it, guarantees that seL4 does provide, go well beyond anything else currently out there.
-
How to write TEE/Trusted OS for ARM microcontrollers?
Take a look at this: https://sel4.systems/
- Simulation: KI-Drohne der US Air Force eliminiert Operator für Punktemaximierung
-
Paragon Graphite is a Pegasus spyware clone used in the US
It's probably have to be seL4 (https://sel4.systems), running on some fully OSS hardware.
There are question marks over much of available RISC-V chips due to chinese producers, so maybe OpenPower based hardware?
Plus, the entire system (motherboard, etc) would need to be manufactured using a good supply chain.
Hmmm, this has probably all been thought through in depth before by others. :)
-
Basic SAT model of x86 instructions using Z3, autogenerated from Intel docs
You can use it to (mostly) validate small snippets are the same. See Alive2 for the application of Z3/formalization of programs as SMT for that [1]. As far as I'm aware there are some problems scaling up to arbitrarily sized programs due to a lack of formalization in higher level languages in addition to computational constraints. With a lot of time and effort it can be done though [2].
1. https://github.com/AliveToolkit/alive2
2. https://sel4.systems/
-
What are the current hot topics in type theory and static analysis?
Formal methods. This is not in most general-purpose programming languages and probably never will be (maybe we'll see formal methods to verify unsafe code in Rust...) because it's a ton of boilerplate (you have to help the compiler type-check your code) and also extremely complicated. However, formal methods is very important for proving code secure, such as sel4 (microkernel formally verified to not have bugs or be exploitable) which has just received the ACM Software Systems Award 3 days ago.
- Rust Now Available for Real-Time Operating System and Hypervisor PikeOS
-
Amiga and AmigaOS should move to ARM.
Today we'd look at seL4.
The-Spiral-Language
-
Does This Language Exist?
Try Spiral for a functional response to the system level programming demands. It has an F#, C, and a Python backend.
-
How do I get around the lack of MailboxProcessor in Fable?
I did the language server for Spiral using Hopac. It involved turning the entirety of what would have been the sequential compilation pipeline into a promise stream.
-
Are there any good resources on reflection in Fable?
Sigh, despite using F# for so long, I've always avoided tackling .NET reflection, but I know from experience (of programming in Spiral) that this is a perfect place to introduce these techniques. Type systems like F#'s really hit their limits when it comes to serializing data across platform and language boundaries, so this is The place to demonstrate the use such methods.
-
why isn't functional more popular?
But a language that support programming in a staged functional programming style, like my own Spiral would actually be very suitable for gamedev, I think more than C# itself. It has compiler guarantees for a lot of things that F# doesn't, and what in other languages would require metaprogramming is just regular programming in it.
-
Ask HN: How do I get the most benefit out of my programming language?
I originally started work on [Spiral](https://github.com/mrakgr/The-Spiral-Language) back in late 2016 because I wanted a functional language in which I could program novel AI hardware that hadn't existed at the time, and still doesn't, but it won't be long before it arrives. It took 3 years of full time work to get it to its current standard of quality, and I'd really feel comfortable programming new hardware devices in my favored functional style. I've designed Spiral so it is both extremely powerful, easy to use while being efficient enough to program devices like GPUs that can't even use heap allocation for their objects.
I am not really concerned about what I'll do when I get access to Tenstorrent chips in six months; my personal needs for the language are met. But I would like it if I could spread the language more broadly, make it useful for people other than myself and get people to sponsor my work on it.
Here is the value proposition of Spiral.
It is a high-level functional PL that has some features that other languages don't, but that isn't really the point. On mainstream devices like the x86 ones there are a lot of programming languages that are good, and it would be tedious to use Spiral to compile to such platforms compared to using such languages directly. It is a bit how ReasonML compiles to JS. Back when I tried it I found using Typescript easier to deal with. So that is not where I'd like to go into, though using Spiral would have benefits in certain areas.
Rather, while reading the [CNX blog](https://www.cnx-software.com/) I realized that while consumer facing AI chips are not here yet, there is a lot of hardware development in the embedded space. They are heterogenous architecture. They have GPU and TPUs in addition to CPUs. And these cross platform interactions within the same system is something that existing languages are really poor at tackling.
If you look at Python or C#, for example, you can't really program the GPU on them directly. They are CPU focused, and don't have the right semantics and would be too inefficient to program devices like GPUs directly. The way I've designed Spiral is that you can program the CPU and the GPU and whatever else from within the same language.
It is not suitable for just GPUs, check this [demo out](https://github.com/mrakgr/PIM-Programming-In-Spiral-UPMEM-Demo). I recently did a backend for UPMEM devices, which are the first commercialized Process-In-Memory chips. I've posted the link to this on HN yesterday and on the Reddit embedded sub, but I got zero interest. And this is really a pity because that map kernel I've demoed is actually a big deal. Back when I first started working on Spiral, it took me 1.5 years of full time work to get to the point where I could write a program like that in the language. And without backend nesting of the kind that Spiral offers, it is impossible to write those kinds of programs no matter how skilled one is as a programmer.
The kind of backend nesting I've demonstrated is not something you can do in F#, Python or any of the languages that I know of. I could easily create such backends for many kinds of hardware. And people would benefit from that because unlike the mainstream computing devices, the hardware coming down the pipeline will have poor language support, nothing on the level of what Spiral offers. For the kinds of heterogeneous architectures I am envisioning, the language designs that are good in the CPU-dominant era, will simply not be suited in the heterogeneous era.
I need chances to demonstrate how good Spiral is, but I am not sure how to get them. If I do not get them, the future of computing will be a lot worse off. I wasn't there when Cuda was incumbent so I missed the boat on that, but I'd like it if Spiral became dominant on future computing devices. Not because I was the one who made the language, but simply because no other design is as suited for them.
-
PIM (Processing-In-Memory) Course
I am not shameless enough to plug Spiral in the main post, but if you are a PIM company or an user of them and want better PL support and tooling, get in touch with me. I'd love to get a chance to play with them.
-
September 2022 monthly "What are you working on?" thread
Two months ago I did a ref counted C backend for Spiral so I might as well plug it now. Since then I've gotten tired of 3d art, and decided to just start writing Heaven's Key.
-
Callbacks without closures?
I just happened to notice that Spiral has a C code generator now. Maybe you can just use that since it's designed with staging in mind and avoiding heap allocation.
-
Multistage Programming / First Class runtime compiler support
Spiral
-
Are there examples of programming language compilers that evaluate the side-effect free parts of the program at compile-time?
Another term to search for is partial evaluation. An interesting language that by default evaluates everything at compile time is Spiral, developed by someone frequenting this subreddit.
What are some alternatives?
l4v - seL4 specification and proofs
lust - A fast, auto-optimizing image server designed for high throughput and caching; Now that is hot.
fprime - F´ - A flight software and embedded systems framework
kuroko - Dialect of Python with explicit variable declaration and block scoping, with a lightweight and easy-to-embed bytecode compiler and interpreter.
nomicon - The Dark Arts of Advanced and Unsafe Rust Programming
gaiman - Gaiman: Text based game engine and programming language
CompCert - The CompCert formally-verified C compiler
exp-flow - experimental rule-based programming formalism under construction [Moved to: https://github.com/contrast-zone/canon]
InitWare - The InitWare Suite of Middleware allows you to manage services and system resources as logical entities called units. Its main component is a service management ("init") system.
cish - Go + Generics + Sum Types
4.4BSD-Lite2 - 4.4BSD Lite Release 2: last Unix operating system from Berkeley
RustScript2 - RustScript is a functional scripting language with as much relation to Rust as Javascript has to Java.