11 ms·

Ask HN: Memory-safe low level languages?

61 points by hyperbrainer 1y ago

I am looking for memory-safe languages that can be used for systems/graphics programming. I love Rust, but it often feels like too massive a language with too much stuff going on. Is there a language like C, which is simpler (obviously without all the UB and other problems)? This is an especially hard ask, given how useful the FP-like features of Rust are, and I find it almost impossible to live without them. Basically, I am looking for a middle ground between C/Zig and Rust. One such language I have found is Austral[0]. What other such languages are there? [0] https://austral-lang.org/

foota 1y ago
It's not really recommended for us, but maybe Carbon?
lproven 1y ago
Pascal (e.g. FreePascal). Modula-2 (e.g. GCC). Oberon (e.g. Oberon, Oberon 2, Oberon-07, Oberon+.)
codr7 1y ago
There have several attempts at cleaning up C without giving up too much of its simplicity; from what I can see, Zig is the only one even close to reaching critical mass. A programming language is always going to make some kind of compromise; better at some things, worse at others. Simplicity/power and safety pull the design in different directions.
- hyperbrainer 1y ago
  I don't mind the language having substantially worse "something" as long as it can be a smaller alternative for Rust, for the lack of a better word. Of course, there always needs to be some compromise. I don't mind that. I just have two requirements, and am curious to see how people have tackled that problem.
  - codr7 1y ago
    Sure, and I'm just as curious. But at the same time, I'm pretty sure that smaller/simpler is going to mean less safe.
    - uecker 1y ago
      I think the opposite is true. The Rust philosophy is the idea that a complicated type system should ensure safety. This may work to some degree, but the overall complexity will introduce new issues. I say this as someone who was really excited about type systems in the past, but Rust is ... meh.
      - hyperbrainer 1y ago
        I think the problem is that some of the more advanced things related to generics or traits are half-baked or maybe somewhat function only in unstable, leading to horribly written code, or code which takes far more complexity to run than it should.
      - SkiFire13 1y ago
        > The Rust philosophy is the idea that a complicated type system should ensure safety. I don't think the "complicated" is part of the philosophy. Rather the idea is that a "strong" type system should ensure safety. The general consequence of this however is that the language becomes quite restricting and limiting. Hence the need for more more complex feature that allow for greater expressibility.
- chrisrodrigue 1y ago
  Zig hits on a lot of Zen of Python. > Beautiful is better than ugly. > Explicit is better than implicit. > Simple is better than complex. > Readability counts. What really sets Zig apart from the usual suspects (C, C++, Rust) is that it has first class compile-time reflection capabilities built into the language (comptime, @field, @typeInfo, etc.) rather than bolted on as macros or templates.
  - 90s_dev 1y ago
    > Python Funny you make that analogy. I remember back when the two contending C alternatives were Zig and Nim, with Nim being syntactically almost a Python clone. It seems Nim has gone the way of Crystal (Ruby version of Nim) and is just kind of there but mostly forgotten and doomed to be abandoned unless it finds a niche. > What sets Zig apart is compile-time I see this claim a lot, but I'm not sure. I think it's the fact that Zig is more or less still C syntax and semantics, just... fixed. The way it does comptime does seem better than how other languages do it, but I haven't actually used it, much less for long enough to judge it properly.
    - aalhour 1y ago
      I haven't used Nim but your comment made me remember that language, yeah it was forgotten but I am not sure if it's completely abandoned, it seems that their team has been launching new language releases on a nice cadence: https://nim-lang.org/blog.html https://nim-lang.org/blog.html
      - cb321 1y ago
        Lately, a lot of work has shifted to nimomy: https://news.ycombinator.com/item?id=43894666 https://news.ycombinator.com/item?id=43894666
    - tauoverpi 1y ago
      Comptime is a gateway to partial evaluation, precomputing tables, and data layout optimization using the same language zig that you're familiar with when you need it and just a convenient way to handle generics when you don't. As an example from my unfinished project, I use it to select the encoding to use [1] when resolving pointers to components [2] to reduce code size [3] as much as possible while keeping a high-level interface [4] where you don't need to care about any of it, just "map" a system over every matching entry within the database and it computes the "best" traversal for a single-thread. This is something that's generally difficult to both keep simple enough to work with and for it to generate good enough code to be worth it while retaining type safety. Comptime enables such without much cognitive overhead as you're working in the same language as before just with lazy evaluation [5] and slightly more lenient rules around memory management making it easier to focus on working towards the desired the data model. [1]: https://codeberg.org/tauoverpi/game/src/commit/77ec827ec93bcbc15a0e6f10837876fb29d43b49/modules/aecs/src/root.zig#L972 https://codeberg.org/tauoverpi/game/src/commit/77ec827ec93bc... [2]: https://codeberg.org/tauoverpi/game/src/commit/77ec827ec93bcbc15a0e6f10837876fb29d43b49/modules/aecs/src/root.zig#L732 https://codeberg.org/tauoverpi/game/src/commit/77ec827ec93bc... [3]: https://codeberg.org/tauoverpi/game/src/commit/77ec827ec93bcbc15a0e6f10837876fb29d43b49/modules/aecs/test/build.zig#L110 https://codeberg.org/tauoverpi/game/src/commit/77ec827ec93bc... [4]: https://codeberg.org/tauoverpi/game/src/commit/77ec827ec93bcbc15a0e6f10837876fb29d43b49/modules/aecs#systems-move https://codeberg.org/tauoverpi/game/src/commit/77ec827ec93bc... [5]: https://godbolt.org/z/P64Ezcrb7 https://godbolt.org/z/P64Ezcrb7
- nielsbot 1y ago
  Related, Apple has a safer C variant they use to build firmware: https://saaramar.github.io/iBoot_firebloom/ https://saaramar.github.io/iBoot_firebloom/
carterschonwald 1y ago
So one kinda cool direction is what they do for the sel4 prject. They have a sequence of high to low level impls and prove correctness wrt spec of the high level etc and prove that each lowering is an implementation of a refinement of the higher level implementation
p_ing 1y ago
C# has been used as the primary language in various hobby/research kernels.
- DaiPlusPlus 1y ago
  > C# has been used as the primary language in various hobby/research kernels. That's quite the oversimplification... C# is not a systems-programming language: it's an application-programming language that is heavily dependent on the CLR runtime environment. While those research-kernels certainly do bring a-kind-of-CLR into the kernel it's far from being like the CLR in .NET; but they don't use C# - at least, not the same C# you use in Visual Studio: those research kernels: Singularity, Midori and Verve - used not only the Sing# and Spec# extensions to C#, they had their own compiler (Bartok) which itself enabled other language-extensions. That said, those extensions are fascinating reads: Sing# concerns message-passing ( https://www.microsoft.com/en-us/research/wp-content/uploads/2006/04/singsharp.pdf https://www.microsoft.com/en-us/research/wp-content/uploads/... ) Spec# added Ada-style (i.e. compiler-enforced) invariants and pre/post-conditions (this was the basis for the Code Contracts feature which was annoyingly/tragically killed-off during the .NET Core reboot in 2016); see https://www.microsoft.com/en-us/research/project/spec/ https://www.microsoft.com/en-us/research/project/spec/ Bartok: https://www.microsoft.com/en-us/research/wp-content/uploads/2008/06/pldi165-chen.pdf https://www.microsoft.com/en-us/research/wp-content/uploads/...
  - p_ing 1y ago
    You've left out Cosmos - https://www.gocosmos.org/ https://www.gocosmos.org/, which itself is primarily written in C#.
  - neonsunset 1y ago
    > C# is not a systems-programming language Incorrect, the main restriction are the targets supported by CoreCLR/NativeAOT/Mono(to an extent). Or, at least, if you pick all memory-safe languages with GC, C# offers the most when it comes to low-level access.
  - gwbas1c 1y ago
    > I am looking for memory-safe languages that can be used for systems/graphics programming. I'm going to assume the author isn't trying to write a kernel.
shakna 1y ago
V [0] aims for something along those lines, but I've had a few issues with the safety aspects of the language. Breaking through the checker isn't that difficult. I absolutely adore Ada [1], but the Pascal-syntax isn't for everyone. I haven't used it yet, but have been hearing rumblings about Odin [2] a fair bit in these kinds of discussions. I tend to avoid too many symbol-heavy langs, but it's probably still less than Rust (I use a screenreader half the time). [0] https://vlang.io/ https://vlang.io/ [1] https://ada-lang.io/ https://ada-lang.io/ [2] https://odin-lang.org/ https://odin-lang.org/
- Cloudef 1y ago
  [flagged]
- n42 1y ago
  I see so much controversy every time V comes up; can someone explain why, without devolving into name calling and personal attacks? What specific design choices or implementation details are contentious, and what legitimate concerns exist beyond interpersonal conflicts?
  - andrewflnr 1y ago
    Having only watched the discussion: The main problem seems to be grossly inflated claims about its capabilities. As in, the docs say it already does X Y and Z, and when you try them they plainly don't work. And then the creator starts with the personal attacks when you point this out.
  - shakna 1y ago
    V... Overpromised, and underdelivered, on what it could do. Promised complete Type Safety, before the type checker was even implemented, for example. As for concerns... The main developer is a concern. Hard to trust them to support the language well, with some of the... Well, tantrums. This isn't aimed at a personal attack. But it is very hard to describe their responses in another manner. This [0] thread on HN covers some of all of the above. But, probably also important to point out that V and its drama have had dang threaten to ban the topic altogether [1]. There's a lot of drama. [0] https://news.ycombinator.com/item?id=39492680 https://news.ycombinator.com/item?id=39492680 [1] https://news.ycombinator.com/item?id=37335249 https://news.ycombinator.com/item?id=37335249
thih9 1y ago
(link from the description, clickable) https://austral-lang.org/ https://austral-lang.org/ > Austral is a new systems programming language. It uses linear types to provide memory safety and capability-secure code, and is designed to be simple enough to be understood by a single person, with a focus on readability, maintainbility, and modularity.
- fpoling 1y ago
  Austral GitHub has not received any significant updates for the last two years so I suppose the language development stopped.
pron 1y ago
If you love Rust -- use Rust. Trying to find a language that's just right for you risks it being just that: right for you and few others. Just remember that even if writing memory-safe programs is your goal, using a memory-safe language is just a means to that goal, and even Rust isn't really memory-safe. Many Rust programs try to achieve memory safety while using a non-memory-safe language (be it C or unsafe Rust), and there's an entire spectrum of combining language features that offer sound guarantees with careful analysis and testing of unsafe code to achieve a safe program. On that spectrum, Zig is much closer to Rust than to C, even though it offers fewer guarantees than Rust (but more than C).
- hyperbrainer 1y ago
  I love Rust, and will continue to use it. But sometimes it feels like "too much". If you have programmed in Rust, you know what I mean. I want to use and experience a language that is to Rust almost like what C is to C++. This is primarily an educational exercise to see how people find compromises that work for them, and languages in the same space as Rust using alternative strategies.
  - api 1y ago
    Rust can feel like "too much" at times. It's a very feature rich language. But that doesn't mean you have to use every feature. With all feature-rich languages I think that's good advice, since code that does use every single feature often ends up being an unreadable mess. Each feature is there for a certain use case, not for every use case.
  - uecker 1y ago
    I do not see any serious contender to C. And considering that most people developing alternative languages that aim to replace C do not seem to have a good understanding what makes a good system programming language, I also do not see this changing soon. Tooling for memory safety will improve and I expect we will also have something complete in ISO C at some point. But already today, one does not have to write modern C as your parents did, e.g. there is no need to do unsafe pointer arithmetic and many other unsafe features can simply be avoided. Signed integer overflow can be checked at run-time. Only temporal memory safety is missing a good solution that ensures safety, but I do not find this is to be a major problem in my projects (with some discipline about pointer ownership)
efficax 1y ago
https://dlang.org/articles/safed.html https://dlang.org/articles/safed.html check out the safed subset of the D language
- fithisux 1y ago
  I second that
- hyperbrainer 1y ago
  Unfortunately, it seems to use a GC for the safety, which makes it unsuitable for a variety of tasks in the systems programming domain. Seems to me like an alternative to Go more than Rust or C or Zig
  - ksec 1y ago
    >it seems to use a GC for the safety, which makes it unsuitable for a variety of tasks in the systems programming domain. That depends. It is really a Hard NO for GC? Crystal is low level enough with a GC and people have written a complete OS with it. On my mobile now so I can't provide link. But it was featured on HN a while ago.
  - skavi 1y ago
    D has a “BetterC” subset that depends only on a C runtime. Presumably there is some overlap with the “SafeD” subset. Curious if there are any D users here who try to stay within that intersection?
  - rurban 1y ago
    On the contrary GC is very suitable to systems programming. The bigger problem is guaranteeing concurrency safety, which you can only provide with nonblocking IO. Everybody loves blocks though, so that's far away.
hardwaregeek 1y ago
If performance is not ultra critical, I'd use Go. It's simple and a small-ish language. Otherwise there's not many options. Not to belittle your question, because it's a good one, but it's a little like asking if there's a simpler aircraft. There can be, but there's a certain amount of required machinery to keep it in the air. Rust's memory safety rules are as simple as we can get it for now. Maybe in a few years it'll be different!
tiffanyh 1y ago
SPARK (Ada) is about as memory-safe as it gets. https://github.com/AdaCore/spark2014 https://github.com/AdaCore/spark2014
- andsoitis 1y ago
  I was also going to suggest Spark https://www.adacore.com/sparkpro https://www.adacore.com/sparkpro There's also this paper, "Memory Safety in Ada, SPARK, and Rust" https://www.adacore.com/papers/memory-safety-in-ada-spark-and-rust https://www.adacore.com/papers/memory-safety-in-ada-spark-an...
  - tiffanyh 1y ago
    I’ve always found the table comparison (Rust/Ada/SPARK) from that same source to be very informative: https://blog.adacore.com/should-i-choose-ada-spark-or-rust-over-c-c https://blog.adacore.com/should-i-choose-ada-spark-or-rust-o...
andrewflnr 1y ago
F-star, which was used to build a verified TLS implementation. https://fstar-lang.org/ https://fstar-lang.org/ Though I guess that's actually on the far side of Rust relative to what you're looking for.
- hyperbrainer 1y ago
  The full language is indeed even further ahead of Rust on the spectrum I am looking at, but this seems like a cool effort. I love proof-based languages and dependent types, so this is an absolute win. What intrigues me quite a bit relative to the main topic of the HN thread is Low[0] > Low is not only a language subset, but also a set of F* libraries that model a curated set of C features: the C memory model, stack- and heap-allocated arrays, machine integers, C string literals, and a few system-level functions from the C standard library. Writing in Low, the programmer enjoys the full power of F for proofs and specifications. At compile-time, proofs are erased, leaving only the low-level code to be compiled to C. In short: the code is low-level, but the verification is not. [0] https://fstarlang.github.io/lowstar/html/Introduction.html#the-essence-of-low https://fstarlang.github.io/lowstar/html/Introduction.html#t...
frizlab 1y ago
Swift can now be used on embedded platforms
pjmlp 1y ago
GCC nowadays offers Modula-2, Ada and D in the box. Then you have FreePascal, as FOSS ObjectPascal dialect. On Apple's turf, Swift naturally, given its bindings for all Metal anything frameworks.
- kristianp 1y ago
  Modula 2 seems to not have libraries for things we might need these days, such as file format support for reading zip and read/write of png, gif, etc. Also TCP/IP comms?
  - pjmlp 1y ago
    There are libraries around, https://github.com/nbrk/m2-raylib https://github.com/nbrk/m2-raylib Naturally given the way it has been largely ignored in the last 30 years, the choice is limited, yet GCC developers considered it had a community big enough to integrate GNU Modula-2 as standard frontend on GCC 14.
tiu 1y ago
See https://wiki.alopex.li/SurveyOfSystemLanguages2024 https://wiki.alopex.li/SurveyOfSystemLanguages2024 and the related discussion https://lobste.rs/s/c3dbkh https://lobste.rs/s/c3dbkh Serious total MSLs that have a defined memory model to allow "low level" operations seem to be scarce if not any. Hence I do not think there is any single one that comes between C/Zig and Rust. I would have said https://www.hylo-lang.org/ https://www.hylo-lang.org/ but, personal opinion, seems like there is too much going on as well. See also https://vale.dev/ https://vale.dev/ P.S Mind mentioning what FP-like features are in Rust? (Genuinely have not looked into Rust that much but I am interested).
qwke 1y ago
https://gleam.run/ https://gleam.run/
gus_massa 1y ago
Have you tried "modern" Fortran? I've seen horrible "old" Fortran programs, but once you add modules it get's much better.
- tiu 1y ago
  I was playing around with Fortran (modern-ish) recently was pretty impressed with the entire ecosystem. `fpm` is really really nice to work, pretty decent LSP server (fortls) as well as good enough documentation. I am not sure however I like the verbosity of it where if you are using 'raw' editors without snippet support, it becomes a chore very soon. All in all it is nice to use and play around with.
noam_k 1y ago
You may want to look at Lua[0]. It's often used as an embedded scripting language in larger projects (and games), has good performance, is memory safe, and is extensible in the same manner as Python (write your performance bottleneck in C/C++). I don't remember specifics, but there are some odd footguns to look out for. [0] https://www.lua.org/ https://www.lua.org/
SkiFire13 1y ago
Have you considered trying one of the older Rust versions (e.g. 1.0.0 or a bit after that) without all the new shiny features?
SloopJon 1y ago
Personally, I don't know what you mean about Rust being too massive. One thing I am wary of is using a truly massive language like C++ on a multi-programmer project without consensus on which features to use and how to use them. Maybe you have in mind something like that? If you want the simplicity of C with more safety, maybe tooling like Frama-C, a MISRA C conformance checker, or just aggressive use of static and dynamic analysis tools like ASAN and UBSAN. You can also disable certain optimizations (e.g., strict aliasing) to steer away from some of the major pitfalls of UB.
MelodyUwU 1y ago
i was actually looking for an answer to a similiar question, so this thread is very much useful! as of now, i looked somewhat at odin
sargstuff 1y ago
Very old school: ASP[0] was old way to do character animations for unix finger command .plan. Recall HN post using python to do the same (handled animation independent of serial terminal speed). Related HN post "John Carmack's .plan file" [3] hascii mation [1]; Use standard graphics techniques and run through [2] or .plan with unscii[4] "sheltered code" via mindcraft : https://youtu.be/7sNge0Ywz-M https://youtu.be/7sNge0Ywz-M ------ ascii animation tutorial : https://www.youtube.com/watch?v=o5v-NS9o4yc https://www.youtube.com/watch?v=o5v-NS9o4yc [0] :Ah, ASP link has been merged with /dev/null. :( ASP and related things for animated .plan : https://superuser.com/questions/253308/scrolling-plan-file [1] : https://github.com/octobanana/asciimation https://github.com/octobanana/asciimation [2] : https://www.geeksforgeeks.org/converting-image-ascii-image-python/ https://www.geeksforgeeks.org/converting-image-ascii-image-p... [3] : "John Carmack's .plan file" : https://news.ycombinator.com/item?id=3367230\ https://news.ycombinator.com/item?id=3367230\ [4] : unscii : http://viznut.fi/unscii/ http://viznut.fi/unscii/
jedimastert 1y ago
Side question and possibly off topic, but is there a formal definition to the term "memory safe"? It seems to mean different things to different people and I'm unsure if I'm just out of the loop and there is an actual definition.
- addaon 1y ago
  A memory safe language is one for which (a) there is a subset of programs which can be statically proven to not perform unsafe memory operations at runtime and (b) no programs outside of this subset will be accepted. The set of operations that are considered to be unsafe can vary, but always includes writes to unowned memory, and often includes reads from unowned and/or uninitialized memory.
mparis 1y ago
I also love rust and we use it heavily at our startup, but I agree with you and wish there were a mainstream alternative that kept much of the type system, pervasive expressions, and pattern matching while being smaller. I’d accept “very fast” even if it’s not as fast as rust. One project I’ve seen that I don’t think is particularly active but that I really like the ideas behind is borgo. It compiles to go (thus GC) but is decidedly more rustacean. Check it out. I hope someone makes something like this wide spread. https://borgo-lang.github.io/ https://borgo-lang.github.io/ PS. I have no affiliation with borgo, just an online fan.
markus_zhang 1y ago
What I dream about is a C with less UB, range based loops, array slicing (supporting negative slicing too), safer and easier string functions (because my pet project is a compiler so gotta write a scanner), pattern matching switch, and maybe a few other stuffs. Oh maybe less preprocessing black magics :/
- ActorNightly 1y ago
  UB issues in C is way overblown. Just don't do dumb shit with null pointers and use const where appropriate that eliminates most of it. As for other stuff, I was working on a LLVM extension a while back to put a lot of Python-isms into C, like the array slicing, print statement, f strings, and decorators. Generally though, I found that writing your own macros is actually easy, and you just have to type stuff out a bit more. Last project I worked on in C I had an include file that had all the macros and the defined functions to go with the macros. The print statement honestly takes up most of the file, cause its a combination of vararg in the macro with _Generic selector with functions defined on how to print each type of variable. But the rest of the stuff like array slicing is just a macro that calls a function that takes the slice arguments as a string. Doesn't look as nice as actual array slicing, but it works and easy to write.
fpoling 1y ago
Vale is interesting, https://vale.dev/ https://vale.dev/ For memory safety compared with Rust it does not use a borrow checker for the price of more checks and extra memory usage at runtime while avoiding GC or even reference counting. I think this is very interesting trade off. Plus there are plans to implement few interesting ideas that even Rust type system cannot implement while keeping the language simple.
cyrc 1y ago
https://cyclone.thelanguage.org/ https://cyclone.thelanguage.org/ How about Cyclone?
- sph 1y ago
  > Cyclone is no longer supported; the core research project has finished and the developers have moved on to other things
khaledh 1y ago
Check out Nim. I'm using it to build an x86-64 kernel¹ (Fusion OS), and it satisfies a lot of the low-level system programming requirements with an elegant and expressive syntax. For memory management you can choose between ARC/ORC and/or manual. It has two downsides though: small community, and the BDFL can sometimes be rough to interact with. ¹https://0xc0ffee.netlify.app/osdev https://0xc0ffee.netlify.app/osdev I, too, have been looking for a unicorn systems programming language, but it doesn't exit yet. Here's what I looked at so far (only languages that don't rely on a GC): - C: lots of UB, less safe (memory- and type-wise) - C++: too complex, not a big fan of OO - Rust: too complex, gets in the way when writing mostly unsafe kernel code - Zig: Good, but syntax is too noisy; lacks interfaces/dynamic dispatch - Swift: Doesn't have a good bare metal story - D: Seems interesting, I may be looking at it (although need to use betterC mode, i.e. not all language features) - Odin: Game programming focused, small but growing community - Ada: Strong candidate, but it has too much ceremony - Pony: I like the capabilities model, but tiny community - Hare: Also tiny community, lacks polymorphism - Hylo (Val): Experimental (mutable value semantics), too immature - Vale: Experimental (regional memory management), seems stalled - V: Good candidate, but mixed reviews on its claims vs. reality - Austral: Experimental (linear types), tiny community, not much progress - Jakt: Built for Serenity OS, not sure if it's getting enough attention - Jai: Focused on game programming, good reviews, but currently closed source (beta) - Mojo: (Python-like) Seems very interesting and I'd give it a try, but too focused on GPU/parallel programming; also too early for adoption
- az09mugen 1y ago
  Thanks a lot for that list ! It matches pretty much what I imagined. On a side note and coming from high-level languages, D is the easiest to learn IMHO, as it is very dev-friendly, mature enough and has a good interoperability with C libraries. I considered for a long time nim for its syntax and "low-levelness", but my lack of knowledge in low-level languages made the learning curve too much steep for me. I think I'll switch to it when I'll have more experience.
sn9 1y ago
You might try OCaml [0] or SML [1] if you want speed, memory safety, and an expressive type system. [0] https://ocaml.github.io/ocamlunix/index.html https://ocaml.github.io/ocamlunix/index.html [1] https://matt.might.net/articles/best-programming-languages/#ml https://matt.might.net/articles/best-programming-languages/#...
oconnor663 1y ago
Can you give some examples of Rust features that you don't need? Unfortunately a lot of common answers (the borrow checker, traits, move semantics) are things that are fundamental to the safety story. I guess one thing you could definitely subtract is async (Rust shipped without it after all).
- whytevuhuni 1y ago
  I would keep lifetime generics, but remove traits and type generics (and therefore the really complex trait bounds, most of the GAT/RPITIT shenanigans, etc). I feel like that would remove most of the complexity, while leaving a mostly C-like language. At most it should have pointer generics (similar to void* or Box<dyn Any>), where the generic function can't assume anything about the data, the data has to be heap-allocated, and the generic function can own and move the pointer around. Enough to implement collections, maybe iteration, and nothing else. Enough to not need monomorphization.
modeless 1y ago
C can be memory safe now! https://github.com/pizlonator/llvm-project-deluge https://github.com/pizlonator/llvm-project-deluge Yes, this is a real project that really works. It can compile real and widely used software written in C including SQLite, OpenSSL, and CPython, giving them true memory safety without escape hatches.
- reirob 1y ago
  Thanks for sharing this. I was not aware about this project. Quite impressive they got sqlite and openssl compiling. From their manifesto [1]: "The biggest impediment to using Fil-C in production is speed. Fil-C is currently about 1.5x-4x slower than legacy C." And for the moment being it is running only on Linux/X86_64, even though there should be nothing preventing it from running on other platforms. [1]: https://github.com/pizlonator/llvm-project-deluge/blob/deluge/Manifesto.md https://github.com/pizlonator/llvm-project-deluge/blob/delug...
musicale 1y ago
C is improving a bit with things like -fbounds-safety https://clang.llvm.org/docs/BoundsSafety.html https://clang.llvm.org/docs/BoundsSafety.html
farseer 1y ago
Use a subset of C++, STL maybe Boost and avoid raw pointers. You will avoid most memory related problems.
gwbas1c 1y ago
> I am looking for memory-safe languages that can be used for systems/graphics programming. C# was kinda-sorta for this; as long as you're targeting an environment where GC is acceptable. (IE, as long as you're running in user-mode, as opposed to writing a kernel or a driver.) It does allow for C-style pointers, which might be useful if you need to call a lower-level system API. (Unfortunately, you can't just suck in a header file.) One thing you might miss is how errors, in Rust, are 0-cost. C# encourages exceptions over error codes, and throwing an exception has a much higher overhead than panic, because it captures a stack trace and allocates an object. (I must admit that I like Rust's error handling over C# because it differentiates cleanly "anticipated" errors versus exceptional situations.)

pron 1y ago
> See Java, it doesn't demarcate unsafe code, you use the unsafe package The use of Unsafe in Java is demarcated, and besides, it is now being removed altogether, but we have more interesting things to talk about. > That means static checks. That means proving properties of your code, implying Rice's theorem. It doesn't. Rice's theorem talks about the undecidability of proving some arbitrary property of arbitrary programs, but given a property, one can construct a language in which it trivially holds for all programs in the language. This is done by finding an inductive invariant -- one that is preserved by all program operations -- that implies the property. Let me give you an example. Due to Rice's theorem, it is undecidable whether or not the output of an arbitrary program that yields a number output is even. Nevertheless, it's easy to construct a language (even a Turing-complete one) where this property always holds. We find a stronger invariant -- all numbers in the program are even -- that can be easily made inductive. Indeed, even numbers are closed under addition, subtraction, and multiplication, while for every division operation we add a runtime check that panics if the result is odd (and, of course, the compiler rejects any literal that isn't even). And voila! Not every program that yields an even output can be written in this language, but every program in this language yields an even output. To see that this is what Rust does with memory safety, note that while every program in safe Rust is memory-safe, not every memory-safe program can be written in safe Rust. > If it's easy (doable) to go 100% memory safe, then there should be a trivial way to always rely on memory guarantees. No need for a spectrum. The need for the spectrum arises because we want to sacrifice 100% memory-safety for other things, such as Java's ability to call C code. > The spectrum exist because rather than writing OS in Ada, programmers collectively decided to bury their heads into C. As someone who wrote safety-critical avionics software in Ada in the nineties, I can tell you that we had good reasons to largely abandon Ada. > an example of Nirvana fallacy. But it isn't because you assume that a language that makes more guarantees will always produce more correct programs per unit of effort, but we know that to be false. From the vantage point of ATS and Idris, a language like Rust is almost indistinguishable from C. There are a few more properties it guarantees than C does, but ATS/Idris can be used to guarantee any program property. If what I said is a nirvana fallacy, then you must not use Rust and always use ATS, because it is much better on your definition of better. The reason we don't is that we know more sound guarantees are not always better, but we didn't always know that. In the seventies, software correctness researchers (such as Tony Hoare) assumed that the only path to scaling software would be soundness (proofs, and even formal proofs). As time went on, we learnt that this belief was false from both sides: unsound methods proved surprisingly effective [1], and proofs proved costly to scale, to the point that they made achieving a required level of correctness more costly. > If you avoid things that are hard, you'll never grow. If a programming language you learned didn't cause headaches, it's not a programming language, it's a dialect. The problem is not in learning new languages. The problem is that more sound guarantees can sometimes reduce the cost of correctness and sometimes increase it. Don't get me wrong: Soundness and proofs sometimes work very well, but we in the software correctness/formal methods world know that things are much more complicated than "more soundness more better". You can read some of my writings on software correctness, after a couple of decades working with formal methods here: https://pron.github.io https://pron.github.io [1]: https://6826.csail.mit.edu/2020/papers/noproof.pdf https://6826.csail.mit.edu/2020/papers/noproof.pdf
- Ygg2 1y ago
  > The use of Unsafe in Java is demarcated, and besides, it is now being removed altogether, but we have more interesting things to talk about. If you call importing a package and using it demarcated, I have a bridge and some fog underneath to sell you. > This is done by finding an inductive invariant -- one that is preserved by all program operations -- that implies the property. This is a strawman fallacy, we're not talking purely theoreticals. Just because you can build a model of Empire state building from Legos doesn't mean that it will work for the real thing. Your Even Theorem Prover can't write 100 beers on the wall. Or even output Hello <name> for arbitrary name. Rust, however, can maintain invariants and be expressive enough because it relies on outside the computer assistance (aka unsafe blocks). > As someone who wrote safety-critical avionics software in Ada in the nineties, I can tell you that we had good reasons to largely abandon Ada. As an outsider looking at commercial and military avionics failures (I can't be certain, but my guess is it seems cost-cutting on both hardware and software didn't quite pan out), I'm not sure that the right call was made. > But it isn't because you assume that a language that makes more guarantees will always produce more correct programs per unit of effort, but we know that to be false. Again, [citations needed]. Google mentioned they had little problem getting people to work with Rust. The onboarding time was around 3 months. And statements that borrow checker is hard is no different, than saying, well, types are hard, generics are hard, covariance & contravariance are hard, indexes starting at 0 are hard, ones and zeroes are hard. To me, these are complaints of people that didn't run the gauntlet, and didn't build their "muscle memory" in programming. > But it isn't because The nirvana fallacy is the informal fallacy of comparing actual things with unrealistic, idealized alternatives.[1] It can also refer to the tendency to assume there is a perfect solution to a particular problem. A closely related concept is the "perfect solution fallacy". You are using ATS and Idris as examples, and I agree, we should use them more. In fact, Rust extensions to generate proofs are amazing in my opinion, and both of those languages are remarkable. What they lack however is an ecosystem. Rust has that. What does Zig give you? No ecosystem, no stability guarantees, and worse memory safety.
  - pron 1y ago
    > This is a strawman fallacy, we're not talking purely theoreticals. No, this is the technique we use in practice in formal methods to prove program properties. When we write a program correctness proof in TLA+ or Lean, this is what we do. This is also how we build invariants into languages. When you learn how to write formal proofs and design type systems, this is what you learn. > Rust, however, can maintain invariants and be expressive enough because it relies on outside the computer assistance (aka unsafe blocks). Rust maintains its invariants by making a stronger invariant inductive in the language. > Google mentioned they had little problem getting people to work with Rust. I am not talking about Rust in particular. I'm talking about your general point that more soundness is always better, and your claim that my argument is an example of a nirvana fallacy because I compare an imperfect solution to a hypothetical perfect one. I am trying to explain that we know that more soundness is sometimes worse for correctness in practice. The problem is not that more soundness isn't perfect, but that there are currently better solutions than more soundness in some situations. You seem to be unaware of the shift in software correctness since the seventies. The gap between the size of programs we can prove correct using deductive methods (currently ~10KLOC) and the size of programs produced in industry is only growing. That is why there's been a shift from deductive proofs to methods such as concolic testing (e.g. KLEE). You can see that by looking at the programs for any software verification / formal methods conference. To be clear, I am not saying that more soundness is never better; I'm saying it is sometimes worse. You can say that we should use ATS more, but the effort of producing software that's proven correct with ATS is not justified by the additional correctness guarantees you gain. I.e., at some point you pay $1000 for improved confidence worth $100.

Ygg2 1y ago
> No, this is the technique we use in practice in formal methods to prove program properties A program that can't express H (72 in decimal) in Hello world is about as divorced from practicals as you can get, without mixing String theory, Meth and Math. > Rust maintains its invariants by making a stronger invariant inductive in the language. Yes, but it relies very little on human verification. > I'm saying it is sometimes worse. And I'm saying it as a programmer field we should monotonically approach the ideal by removing languages that don't support it. A language that has memory safety issues is worse than a language that doesn't. We had hundreds of example in practice where people just can't write/compose safe code. C has a 50 year history and most of the active projects in it are mired in memory safety issues. Also seatbelts are sometimes worse, doesn't mean we shoud abolish them for seatbelts-less Pintos.
- pron 1y ago
  > A program that can't express H (72 in decimal) in Hello world is about as divorced from practicals as you can get Huh? I was giving an example of how we make undecidable properties trivial in languages. It can be any property. It's easy to see that Rust does the same with memory safety, i.e. through an inductive invariant, because every statement in Rust maintains the invariant. > Yes, but it relies very little on human verification. Of course. It shouldn't rely on human verification at all. That's how we design type systems. But because an inductive invariant is inherently conservative and must reject correct programs, there is additional human effort required -- not to verify the property, but to stay within the confines of the inductive invariant. In Rust terms, the compiler takes care of memory safety, but you need to put an effort into expressing memory-safe programs in Rust to fit within Rust's constraints, which are, necessarily more restrictive than memory safety (because they must use an inductive invariant). > And I'm saying it as a programmer field we should monotonically approach the ideal by removing languages that don't support it. And I'm saying that what we've learnt over the past five decades is that more soundness does not necessarily mean getting closer to the ideal. Sometimes more soundness gets us further away from the ideal. > Also seatbelts are sometimes worse, doesn't mean we shoud abolish them for seatbelts-less Pintos. No one is suggesting that, it's just that what you're referring to as seatbelts could sometimes do more harm than good even for safety. We have empirical evidence that real seatbelts increase safety; things are nowhere near as clear for language soundness. Sure, C is so exceptionally weak that we can do better than that, and there's no doubt Rust is better on correctness than C, but that's not the same as saying Rust is better on correctness than any language that makes fewer guarantees than Rust. Why? Because, again, we've seen that the benefits of soundness are not linear -- they help until they start hurting. Knowing where that point is is not easy.
  - Ygg2 1y ago
    > Huh? I was giving an example of how we make undecidable properties trivial in languages. It can be any property. Yes, but insisting you have to be 100% machine verified, while the program is correct, it is impractical. While it might be Turing complete, it can't express equivalent behavior to a C program. This is one of those quotes like "Don't let perfect be the enemy of good". Look at your definition of memory safety, by it nothing other than ATS or some Lisp derivative running on a Lisp machine is actually memory safe. Sure, it's theoretically sound, but it's not pragmatical. > We have empirical evidence that real seatbelts increase safety; things are nowhere near as clear for language soundness. We have empirical evidence that Rust has measurable impact on bugs, especially memory safety ones.
    - pron 1y ago
      > While it might be Turing complete, it can't express equivalent behavior to a C program. Neither can safe Rust! But this is easier to see in my example because parity is a very functional, as opposed to technical property. > This is one of those quotes like "Don't let perfect be the enemy of good". I am not calling for perfect. Quite the opposite. I am saying that software correctness is extremely complicated, and even the biggest researchers in the field have been surprised by outcomes that were counterintuitive to them. Yet you seem to have decided that Rust gives the best results of everything that's available, while I have my doubts, especially because I see how people are turning away from Rust and how much it struggles to capture a significant portion of the low-level programming market even at its quite advanced age. I don't think there's a single language in the top ten that's had such low adoption at Rust's current age, and that's not the kind of thing you expect to see with a technology whose excited but small fanbase claim to hit an excellent pragmatic sweet spot. > We have empirical evidence that Rust has measurable impact on bugs, especially memory safety ones. Compared to C, yes. That's exactly what you expect if more sound guarantees help and then hurt -- a language with some sound guarantees to be better than a language with virtually none. But that is not to say that other languages with either more or less sound guarantees aren't an even better sweet spot.