seL4
nocode
seL4 | nocode | |
---|---|---|
60 | 108 | |
4,549 | 59,455 | |
1.2% | - | |
9.0 | 0.0 | |
3 days ago | 26 days ago | |
C | Dockerfile | |
GNU General Public License v3.0 or later | Apache 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.
nocode
-
I'm Excited about Darklang
> "no cruft: no build systems, no null, no exception handling, no ORMs, no OOP, no inheritence hierarchies, no async/await, no compilation, no dev environments, no dependency hell, no packaging, no git, no github, no devops: no yaml, no config files, no docker, no containers, no kubernetes, no ci/cd pipelines, no terraform, no orchestrating, no infrastructure: no sql, no nosql, no connection poolers, no sharding, no indexes, no servers, no serverless, no networking, no load balancers, no 200 cloud services, no kafka, no memcached, no unix, no OSes"
I'll be honest, I did the same and at first thought Darklang was a troll project along the lines of https://github.com/kelseyhightower/nocode.
Either this is one hell of a project that is taking on all problems (and will consequently fail), or this pitch is misguided. The majority of what is listed there have nothing to do with languages.
-
Thinking Inside The Box: Relational Style Joins in SurrealDB
I hope this clears some of the fears of missing out (FOMO) that you might have about SurrealDB not having traditional SQL joins. You can still do the things you need to do such as with the subqueries. When it comes to the traditional joins though, we think about it more in terms of the joy of missing out (JOMO) because the best way to reduce errors in your code is by writing less code, as seen in our record links example.
-
Vanilla Design: The Best React UI Library Ever
Vanilla Design is a super lightweight, ultra high-performance React UI library. Vanilla Design Team places a great emphasis on code size and performance, drawing inspiration from the nocode philosophy, which has significantly boosted the security and maintainability of Vanilla Design. It's like they've added an extra layer of bulletproofing and polish to their creation!
- efficiencyHack
-
Ask HN: How Airtable / Notion's Database is implemented?
There are some open source competitors to Airtable and Notion that can provide good insight. Check out https://github.com/kelseyhightower/nocode
-
Does Debian always have this many "release critical" bugs at release?
Well 100 is a number. And here is the relation: https://sources.debian.org/stats/ and here is how to get 0 bugs: https://github.com/kelseyhightower/nocode
-
Looking for partner to start hosting service
This is my background and i years of experience hosting this..
-
Sunt masterele online worth it?
Asta kelseyhightower/nocode: The best way to write secure and reliable applications. Write nothing; deploy nowhere. (github.com) are mii de forkuri si zeci de mii de stelute, activitate masiva la 'issues' - mii, sute de 'pull requests', clar ca rezolva o problema reala, nu?
-
My manager wants me to code a bug free application
Well, you can write a bug-free application..
-
Show HN: Gut – An easy-to-use CLI for Git
First off, congratulations on entering the Computer Science!
Second, I am not sure what is a bigger joke here, the project itself and the OP's innocuous and cute self-promotion or the fact that this post landed the HN's front page.
0. Terms and definitions.
"You" refers not to the author of the tool but to the dear reader who happens to stumble upon this comment in the stream of random screen scrolling.
1. Comment body.
Couple of things about CS classes and specifically about programming classes. They will teach you everything but the most important engineering principles. And you'll have to adjust your learnings once you leave the campus gate behind and enter the wilderness of real tasks and challenges.
The first biggest lesson I learnt as a CS graduate was that the most beautiful, efficient and valuable software program is the one that does not exist, literally no code[0]
The second biggest lesson I learnt as a CS graduate was YAGNI[0]. You never ever write a single line of code, even touch the keyboard until you are absolutely sure you have exhausted all possible options to solve your problem without getting your hands dirty with programming.
The third biggest lesson I learnt as a CS graduate was RTFM[2]. It is so exciting to go to conferences and see people present fancy slides and watch youtube videos with lollipop coloured pictures explaining some complex topics in a eli5 style. Or read blog posts on a gazillion of websites posted by unknown unknowns but yet coming so convincing as if they were written by John Carmack or ChatGPT 5. But then none of them tell you the whole truth and show you the full picture. It is only official documentation, manuals and boring reference specifications that can help you find what you are looking for. And you will need to learn the skill of grinding hunderds of pages of badly styled refdocs to find that really nitty gritty quirky feature that consumed your whole day in finding out why your code does not work as expected. That's where you will start proceeding to the official docs and source code (if needed) before anything else (even Stackoverflow!).
There have been so many git wrappers around, you can probably try them all (tig, jj, gh-cli, gitui, lazygit, gix, you google it). But then, no matter how much effort their authors invest in those tools, there will always be inconsistency between git and its wrapper and you find yourself resorting to git to do what was supposed to be covered by the bespoke tool. And then you learn to respect git, understand its concepts as they were designed, learn some bash and git aliases[3], ditch all those tools (or the majority of them) and proceed with your personal tailored toolbox where if you find something odd you adjust it for your needs within 10 minutes and chill out.
[0] - https://github.com/kelseyhightower/nocode
[1] - https://en.wikipedia.org/wiki/You_aren%27t_gonna_need_it
[2] - https://en.wikipedia.org/wiki/RTFM
[3] - https://git-scm.com/book/en/v2/Git-Basics-Git-Aliases
What are some alternatives?
l4v - seL4 specification and proofs
Motor Admin - Deploy a no-code admin panel for your application in less than a minute. Stop wasting time on custom internal tools and focus on the actual product. Motor Admin allows to launch a custom admin panel for any application.
fprime - F´ - A flight software and embedded systems framework
swagger-core - Examples and server integrations for generating the Swagger API Specification, which enables easy access to your REST API
nomicon - The Dark Arts of Advanced and Unsafe Rust Programming
ArnoldC - Arnold Schwarzenegger based programming language
CompCert - The CompCert formally-verified C compiler
fpcupdeluxe - A GUI based installer for FPC and Lazarus
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.
fetlang - Fetish-themed programming language
4.4BSD-Lite2 - 4.4BSD Lite Release 2: last Unix operating system from Berkeley
lowdefy - The config web stack for business apps - build internal tools, client portals, web apps, admin panels, dashboards, web sites, and CRUD apps with YAML or JSON.