9 ms·
Nvidia Security Team: “What if we just stopped using C?” (2022)
- r1chardnl 2y agoAfter briefly skimming through their talk they mention they're a third party consultancy company making recommendations on safety for NVIDIA, so "Nvidia Security Team" take it how you will. Also I think these drastic changes moving towards a completely different language always bug me, especially when the syntax is also completely different. Then there's like everything libraries wise and CUDA is all C/C++ if I'm not mistaken. In every large project I'm sure you're eventually going to find some exploit attack vector. Especially if the focus from what I believe for GPU/CUDA until recently wasn't mostly focused on security rather than performance and those are always trade-offs.
- kortilla 2y agoYeah, it completely loses all weight when it’s an external consultancy suggesting it. It’s easy to say “rewrite everything in X because Y” when you don’t have to deal with the burden of figuring out how to do that. Flagged the article because the title is super misleading.
- transpute 2y ago> Flagged the article because the title is super misleading From the case study, the question was posed by Nvidia employees, before finding Ada/SPARK and Adacore, https://news.ycombinator.com/item?id=43043381 https://news.ycombinator.com/item?id=43043381 NVIDIA began to ask themselves, “Can we change our fundamental approach? And if so, which of these tools can we actually use?” They put these questions to their software security team. In reply, the security team came back with what Daniel Rohrer characterized as “a fairly heretical” proposition: “What if we just stopped using C?” This led to other questions, like, “What alternative languages and tools are available to support the use of formal methods?” In trying to answer those questions, NVIDIA discovered SPARK.
- touisteur 2y agoThe focus of their work seems to be low-level firmware, and not CUDA or any kind of compute. It makes sense a lot there because you won't need as many libraries. The syntax is really a red-herring especially when you get contracts, proof of absence of runtime errors and higher-lever functional proof, mostly automated, or assisted with annotations. If you're actually going with this effort, the lack of curly braces, ampersands shouldn't be a main concern.
- indolering 2y agoAda's refusal to make their language any more approachable is a problem.
- yjftsjthsd-h 2y agoWhat's unapproachable about it? And if your answer involves syntax, how do you explain Python?
- bluGill 2y agoMostly I have no clue how I would use it in my project without rewriting from scratch.
- yjftsjthsd-h 2y agoYou either write the main program in C and call Ada libaries, or you write the main program in Ada and call C libaries: https://learn.adacore.com/courses/intro-to-ada/chapters/interfacing_with_c.html https://learn.adacore.com/courses/intro-to-ada/chapters/inte... (And this seems pretty general; you'd have to do roughly the same thing to mix C/Rust, C/Pascal, Rust/Python, ...)
- bluGill 2y agoProblem is my main program is c++ complete with the stl that makes it useful. Vectors unique-ptr and all the other weird stuff that makes c++ better that c.
- Joel_Mckay 2y agoIn general, NVIDIA never had proper bug-free support in C for well over a decade (hidden de-allocation errors etc.), and essentially everyone focused on the cuda compiler with the C++ API. To be honest, it still bothers me an awful GPU mailbox design is still the cutting-edge tech for modern computing. GPU rootkits are already a thing... Best of luck =3
- einpoklum 2y ago> with the C++ API The funny thing is that the "C++ API" is almost entirely C-like, foregoing almost everything beneficial and convenient about C++, while at the same time not being properly limited to C. (which is why I wrote this: https://github.com/eyalroz/cuda-api-wrappers/ https://github.com/eyalroz/cuda-api-wrappers/ ) > an awful GPU mailbox design is still the cutting-edge tech Can you elaborate on what you mean by a "mailbox design"?
- Joel_Mckay 2y agoIn general, a modern GPU must copy its workload into/out-of its own working area in vram regardless of the compute capability number, and thus is constrained by the same clock-domain-crossing performance bottleneck many times per transfer. At least the C++ part of the systems were functional enough to build the current house of cards. Best of luck =3
- pjmlp 2y agoDepends on which CUDA API one is looking to, https://docs.nvidia.com/cuda/cuda-c-std/index.html https://docs.nvidia.com/cuda/cuda-c-std/index.html
- einpoklum 2y agoI meant the fundamental ones, mostly: * CUDA Driver API: https://docs.nvidia.com/cuda/cuda-driver-api/index.html https://docs.nvidia.com/cuda/cuda-driver-api/index.html * NVRTC: https://docs.nvidia.com/cuda/nvrtc/index.html https://docs.nvidia.com/cuda/nvrtc/index.html * (CUDA Runtime API, very popular but not entirely fundamental as it rests on the driver API) the CUDA C++ library is a behemoth that sits on top of other things.
- bsder 2y agoYeah, when I see the equivalent to slang written in Ada/Spark, I'll actually believe them.
- 0xbadcafebee 2y agoI forget sometimes that the papers and talks issued by teams at most companies are for PR and resume-padding. They hype the findings that justify that team's budget, and bury any negatives. The other funny thing I noticed is the formal verification just means the program implements the standard - it doesn't mean the standard doesn't have security holes! And sometimes the security holes are implementation-specific, like timing attacks, which can require weird low-level tricks to solve.
- edelbitter 2y ago>bury any negatives I was looking for the x86-specific rant, and did not find it. You'd think that team would have had something to say about architecture complexity.
- transpute 2y agoNvidia’s GPU root of trust, where they are using SPARK, is based on RISC-V, they have a talk about that choice, https://news.ycombinator.com/item?id=43045952 https://news.ycombinator.com/item?id=43045952
- transpute 2y ago> After briefly skimming through their talk they mention they're a third party consultancy company making recommendations on safety for NVIDIA, so "Nvidia Security Team" take it how you will. This is a marketing case study by the major Ada tools and training vendor, on years of engineering work done by their customer, Nvidia. It includes quotes from Nvidia employees and their blog references a Defcon video by the head of the Nvidia Offensive Security team, https://www.adacore.com/uploads/techPapers/222559-adacore-nvidia-case-study-v5.pdf https://www.adacore.com/uploads/techPapers/222559-adacore-nv... Principal Software Engineer Manager, GPU Firmware Security Senior Manager, GPU Software Security VP, Software Security At the conclusion of their initial POC at the end of 2018, NVIDIA had five developers trained in SPARK. By the second quarter of 2022, that number had grown to over fifty.. Several NVIDIA teams are now using SPARK for a wide range of applications that include image authentication and integrity checks for the overall GPU firmware image, BootROM and secure monitor firmware, and formally verified components of an isolation kernel for an embedded operating system.
- zifpanachr23 2y agoMaybe it's naive of me but I also don't really perceive much of a security imperative for NVIDIA. They make graphics cards and slop generator cards for the most part. What exactly is the threat model here that requires switching to prioritizing memory safety? Are there a lot of graphics card related codes that are being exploited in the wild?
- guipsp 2y agoAre you aware of how the nintendo switch got piracy?
- transpute 2y agoNVIDIA GPU RISC-V root of trust is analogous to Apple T2 secure enclave, AMD PSP, or Intel ME, which all perform security-critical functions. > What exactly is the threat model here It probably varies by product, but one commercial possibility is protection of price premiums, e.g. enforce feature segmentation for different products or customers, while using common silicon. NVIDIA operating margin reached 50%, unusually high for a hardware company, https://www.macrotrends.net/stocks/charts/NVDA/nvidia/operating-margin https://www.macrotrends.net/stocks/charts/NVDA/nvidia/operat.... AMD margin is below 20%. 2021, https://www.youtube.com/watch?v=l7i1kfHvWNI https://www.youtube.com/watch?v=l7i1kfHvWNI 2024, https://static.sched.com/hosted_files/riscvsummit2024/fe/Keynote_2024.pdf https://static.sched.com/hosted_files/riscvsummit2024/fe/Key... ~1 Billion RISC-V cores shipping in 2024 NVIDIA chips Unified embedded HW and SW across all NVIDIA products • Eliminates replication in basic primitives (isolation, crypto etc.) • Maximizes SW/HW leverage across NVIDIA Configuration: pay only for what is needed Custom extensions: additional functionality, security, and performance Our HW and SW architecture enable differentiation There are upcoming open hardware/firmware RoT building blocks like OpenTitan (RISC-V), OCP Caliptra and TockOS (Rust) that could be used by competing device and platform vendors. > don't really perceive much of a security imperative for NVIDIA When countries start budgeting hundreds of billions of dollars for national investment in LLM-based AI based on GPUs, they may introduce new security requirements for the underlying infrastructure.
- tonyarkles 2y ago
- kqr 2y ago> moving towards a completely different language always bug me, especially when the syntax is also completely different. Why do syntax differences bug you? I could understand most concerns about switching ecosystems, but surely the difference between e.g. C++ and Java and JavaScript are orders of magnitude larger than that between C++ and Ada. Syntax is the smallest piece of it all, as far as I'm concerned. > Then there's like everything libraries wise and CUDA is all C/C++ if I'm not mistaken. Ada has excellent C interop.
- ForOldHack 2y agohttps://news.ycombinator.com/item?id=27317403 https://news.ycombinator.com/item?id=27317403 !!!
- jasonpeacock 2y agoThey used SPARK instead: SPARK is a formally defined computer programming language based on the Ada programming language, intended for the development of high integrity software used in systems where predictable and highly reliable operation is essential. It facilitates the development of applications that demand safety, security, or business integrity. https://en.wikipedia.org/wiki/SPARK_(programming_language) https://en.wikipedia.org/wiki/SPARK_(programming_language)
- roenxi 2y agoPeople who don't want to read the first line of the article, rejoice! It sounds like a good decision though. Formal verification tends to make more sense in highly concurrent situations where there is a high-value stable API to be supported. That describes graphics cards and surrounding environments really well so it makes sense that Nvidia would find use cases. Something more from the article is also that they made the decision with a pilot project that went well. It'd be nice to have more details about it; that sort of thing is important to do well and always interesting. Lo and behold, we do have more details about it! https://blog.adacore.com/when-formal-verification-with-spark-is-the-strongest-link https://blog.adacore.com/when-formal-verification-with-spark... - there is a video in there that looks to be worth a watch.
- MichaelDickens 2y agoNothing in the article explained what SPARK is. I appreciated GP's comment.
- rs186 2y ago[flagged]
- Tadpole9181 2y agoI'm with you in spirit, but NVIDIA Spark is a thing insofar as RAPIDS? https://www.nvidia.com/en-us/deep-learning-ai/solutions/data-science/apache-spark-3/ https://www.nvidia.com/en-us/deep-learning-ai/solutions/data...
- bitwize 2y agoWow, was not expecting Boomer Rust to take center stage here. Awesome results by the security team.
- indolering 2y agoThat's an incredible title!
- bitwize 2y agoYeah, I gave a talk on Ada a few months back at a local meetup. Calling it "Boomer Rust" at the start helped break the ice, everyone laughed, and it also helped them get the gist of Ada's particular value-add while I went into details.
- harry8 2y agoAda = Boomer Rust <==> Rust = Millennial Ada I can imagine Boomers laughing but the Rustaceans not seeing the humour in it at all. I could be wrong...
- sgt 2y agoMillennials are getting old though. When is Gen Z going to build a language? They probably won't though, because it's hard to ask an AI to build a brand new Ada for you.
- xvilka 2y agoSadly, Rust still lacks some features that Ada has. For example, range types[1] (a narrow case of the dependent types). [1] https://en.wikibooks.org/wiki/Ada_Programming/Types/range https://en.wikibooks.org/wiki/Ada_Programming/Types/range
- bitwize 2y agoIn my talk I expounded on how people were concerned with safety even in the 80s, and how Ada provides tools to construct programs that were safe in many other ways besides just memory safety.
- NavinF 2y agoArticle doesn't say what parts of Nvidia's stack use SPARK. Considering Nvidia is a huge software company with ~30,000 employees, "There are now over fifty developers trained and numerous components implemented in SPARK" doesn't inspire confidence. IMO the realistic path towards formal verification is AI proof assistants that automate the tedious parts instead of forcing you to write your code in a weird way that's easier to prove
- antirez 2y agoTotally agree that AI is going to have a huge impact on security of languages, and will change many paradigms.
- mr_toad 2y agoThere are probably 50 developers working on the actual drivers and several thousand on GeForce Experience.
- sdwr 2y agoDon't they release custom tuning patches for every single AAA game that comes out? Geforce Experience is basically just a spoonful of sugar to make sure people install new drivers.
- dogma1138 2y agoI’m not entirely sure they are writing any portion of their driver using SPARC the presentation they gave 5 years ago seems to indicate they are limiting the usage to firmware for their embedded RISC-V co-processor, they may have expanded the usage of it but I still think it’s predominantly firmware related with possibly some expansion to their automotive and robotics solutions. https://www.slideshare.net/slideshow/securing-the-future-of-safety-and-security-of-embedded-software/217232842 https://www.slideshare.net/slideshow/securing-the-future-of-...
- alexashka 2y ago[flagged]
- einpoklum 2y agoTBH, this sounds like somewhat of a nothing-burger published by an organization with a motivation to overstate the use of Ada / Spark. Specifically, the article does not claim that any significant bit of code at NVIDIA uses SPARK or Ada.
- uxp100 2y agoSignificant bits of code at NVIDIA use SPARK. Small percentage of total code written, but in significant places.
- einpoklum 2y ago> Significant bits of code at NVIDIA use SPARK. That is a vacuous statement, because: * We don't know what constitutes "significant" * We don't know what it's significant _for_ * "code at NVIDIA" is an extremely wide definition.
- transpute 2y agoDetails, slides and video are in this HN discussion, linked from sibling response. vacuous: Devoid of substance or meaning; vapid or inane. disingenuous: Pretending to be unaware or unsophisticated; faux-naïf. guarded: Cautious; restrained.
- transpute 2y agoThe linked Nvidia case study names GPU firmware components, https://news.ycombinator.com/item?id=43043541 https://news.ycombinator.com/item?id=43043541
- chadcmulligan 2y agoAny Spark compiler? I've found https://www.adacore.com/sparkpro https://www.adacore.com/sparkpro which says request pricing - never good, any open ones suitable for playing with?
- ajxs 2y agoThere's a GPL version of GNATprove, which you can install with Alire (https://alire.ada.dev https://alire.ada.dev). That's the version I use.
- MaxBarraclough 2y agoYou wouldn't guess it from AdaCore's homepage, but SPARK tooling (including provers) and the GNAT Ada compiler are both made freely available, with the goal of attracting interest from FOSS projects. Here's a page on this: https://blog.adacore.com/a-new-era-for-ada-spark-open-source-community https://blog.adacore.com/a-new-era-for-ada-spark-open-source... ajxs is right to say that the way to get your hands on this tooling is to use the Alire package-manager. AdaCore no longer offer alternative means of distribution (except, presumably, to paying customers).
- LeFantome 2y agoPretty huge promotional opportunity for AdaCore. You can tell because this was written by AdaCore. Still, I am a bit convinced. The NVIDIA name is increase the chance that I will evaluate SPARK sometime soon. I have to admit, other than knowing it exists, I am not super familiar with it. What I have seen before now has felt like them using the popularity of Rust as a platform for promotion. This, at least, appears to be a use case where they came in on their own merits.
- transpute 2y ago> huge promotional opportunity Right? Yet they published this customer case study in 2022 and it never reached HN. Found in 2025 search on GPU firmware security.
- 8organicbits 2y agoIt's hard to tell what components are now written in spark. The driver is mostly c, and none of the open source repos are identified as spark. https://github.com/NVIDIA/open-gpu-kernel-modules https://github.com/NVIDIA/open-gpu-kernel-modules https://github.com/NVIDIA/ https://github.com/NVIDIA/
- transpute 2y agoTheir PDF has a bit more detail, https://news.ycombinator.com/item?id=43043541 https://news.ycombinator.com/item?id=43043541
- cxr 2y agoI maintain conviction in my position that if AdaCore and/or other champions of Ada were to undertake a serious project (i.e. not an April Fools' Day joke blog post[1]) to ship a compiler that accepts a curly-braced dialect of the language[2][3], then there would be at least twice as many new, earnest users of the vulgar "skinned" form as there are programmers today using the existing language, and that this tripling would happen virtually overnight. I'm not even talking about major revisions to the grammar. I'm saying fork the lexer to accept a different set of terminals, and leave the nonterminals alone. Is this stupid and unreasonable and should programmers just get over themselves and use a language on the strength of its merits instead of being turned off by surface-level stuff? Yeah, it is, and yeah, they should. But people are fickle. 1. <https://blog.adacore.com/a-modern-syntax-for-ada https://blog.adacore.com/a-modern-syntax-for-ada> 2. <https://news.ycombinator.com/item?id=24367358 https://news.ycombinator.com/item?id=24367358> 3. <https://news.ycombinator.com/item?id=35217839 https://news.ycombinator.com/item?id=35217839>
- juped 2y agoI'm also desperate to stop Rust by any means, but I don't think you're correct; I think the sticking point for language adoption is the presence or absence of a big npm clone.
- steveklabnik 2y agoAlire has existed for a long time now; the oldest release on GitHub is 0.4 from 2018.
- coliveira 2y agoNothing prevents anyone from creating a preprocessor that maps { to BEGIN and } to END.
- cxr 2y agoNothing prevents anyone from trying to eat spaghetti with a spoon. (Or from modifying the lexer to accept a different set of terminals, even.) > Kramer: "Yeah, well, I could do it. I don't wanna do it." > Jerry: "We didn't bet if you wanted to do it. We bet on if it would be done." > Kramer: "And― and it could be done." > Jerry: "Well of course it COULD be done. Anything COULD be done. But it's only is done if it's done! Show me the levels! The bet is the levels!" > Kramer: "I don't want the levels!" > Jerry: "That's the bet!" <https://www.youtube.com/watch?v=4CxIVvLaGKI https://www.youtube.com/watch?v=4CxIVvLaGKI>
- PaulHoule 2y agoEfficiency of Ada should be pretty close to C, but that strange thing Ada does where you define your own numeric types like type Day_type is range 1 .. 31; creeps me out a little, it makes me think I have to throw Hacker's Delight [1] in the trash if I want to use it but I could be wrong. It makes me think of the the deep history of computing, where there were a few straggler architectures (like the PDP-10 [2]) that didn't use the 8-bit byte were around and when Knuth wrote a set of programming books based on an instruction set that wasn't necessarily binary. (Lately I was thinking about making a fantasy computer that could be hosted in Javascript which was going to be RISC but otherwise totally over the top, like there would be bitwise addressing like the PDP-10. First I wanted it to be 24 bit but then I figured I could pack 48 bits in a double so I might as well. It even would have a special instruction for unpacking UTF-8 characters and a video system intended for mixing latin and CJK characters. Still boils down to an 8-bit byte but like the PDP-10 it could cut out 11-bit slices or whatever you want. I was going to say screw C but then I figured out you could compile C for it) [1] https://en.wikipedia.org/wiki/Hacker%27s_Delight https://en.wikipedia.org/wiki/Hacker%27s_Delight [2] https://en.wikipedia.org/wiki/PDP-10 https://en.wikipedia.org/wiki/PDP-10
- taurknaut 2y agoThis doesn't strike me as that different than an enum.
- MathMonkeyMan 2y agoArithmetic is defined on range types. So day 30 + day 4 is 34, which if you then try to coerce into a day will throw an exception.
- dragonwriter 2y agoAnd... So? It seems you are saying Day_type + Integer is Integer, and Integer (in general) cannot safely be coerced into Day_type and... that’s logically correct?
- 2y ago
- TZubiri 2y ago"Testing security is pretty much impossible. It’s hard to know if you’re ever done,” "We wanted to emphasize provability over testing as a preferred verification method" Yet another developer seeking a panacea that will allow them to keep their job while diminishing their workload. For typical workers, it's a fact that work is infinite, so you put your 8 hours and then do it again the other day. Whenever devs get put in this position they go for the nuclear option of going for the moon. Man just keep finding bugs to the best of your ability, it will never be 100% secure, except insofar as you gerrymander what's a vulnerability and what is your responsibility. Good luck. But if I have to put my chips in Nvidia's VP vs C, I put them in C. The list of C contenders has been long, and it seems more likely that the vp is at the peak of their life ala musk or altmann and they have their own delusions. Not sure whether going to mars is crazier or whether finally replacing C is.
- tombert 2y agoI've never used SPARK, but the Wikipedia page makes it seem pretty interesting. For that matter, Ada seems interesting, I kind of wish it had caught on outside of the defense industry.
- numeromancer 2y agoIt failed to catch on outside the defense industry because that is where is started. It was long sneered at as a "language designed by committee". In one programming class, in college, we used a text-book called "Oh my, Modula 3!". On the back they explained the title, saying "better 'Oh my, Modula 3!' than 'Oh no, Ada!'".
- tombert 2y agoYeah, people have explained to me here before. It's just too bad, because Ada looks like a language that should have gotten more popular. I was playing with some of the concurrency constructs built into it, and it was fairly pleasant, and it makes me think about the "what if?" universe where it caught on instead of C++ dominating the 90's and 2000's.
- timbit42 2y agoYou mean, "Oh My! Modula-2!", not 3. The title of that book was chosen as a reference to a previous book titled, "Oh! Pascal!".
- dang 2y agoDiscussed at the time: Nvidia Security Team: “What if we just stopped using C?” - https://news.ycombinator.com/item?id=33504206 https://news.ycombinator.com/item?id=33504206 - Nov 2022 (362 comments)
- white-flame 2y agoThe real problem is deeper than this. The actual question to ask is: "What if we just stopped distributing and blindly executing untrusted binary blobs?" A trusted compiler in the OS, and some set of intermediate representations for code distribution would solve a massive amount of security issues, increase compatibility, and allow for future performance increases and disallowing suspect code patterns (spectre, rowhammer, etc). Specializing programs at install time for the local hardware makes way more sense than being locked into hardware machine code compatibility.
- bawolff 2y agoI feel like you might as well ask "why not world peace"? There are a huge number of practical issues to be solved to make that be viable.
- grayhatter 2y agocould you list a few of the problems you predict?
- tsimionescu 2y agoThat does nothing to fix the vast majority of security issues, which are caused by trusted but not memory safe programs running on untrusted input. It's also an extremely unrealistic goal. First of all, you run into a massive problem with companies and copyright. Second of all, it will be very hard to convince users that it's normal for their Chrome installation to take half an hour or more while using their CPU at 100% the whole time.
- transpute 2y agoFor a while, Apple required apps to be submitted as bitcode (LLVM IR) to the App Store, where they would be converted to x86 or Arm machine code during device install. They stopped that a couple of years ago, after migration to Apple Silicon.
- refulgentis 2y agoApple used to require bitcode (LLVM IR) for App Store submissions. Rest is interesting, nothing was done on install, it wasn't converted or anything to machine code. In fact, in practice, it never ended up being used. Well, that's not particularly relevant: the idea was never to do something on device anyway. Really excellent post here summarizing that I can vouch for: https://stackoverflow.com/questions/72543728/xcode-14-deprecates-bitcode-but-why https://stackoverflow.com/questions/72543728/xcode-14-deprec...
- skirge 2y ago""Beware of bugs in the above code; I have only proved it correct, but didn't test it"
- randomNumber7 2y agoYes, lets just use pascal. Who needs dynamic memory allocation and functions that can take strings of multiple length?
- bawolff 2y agoWe are talking about firmware. I am just a web dev and dont know much about the embedded space, but my impression was that dynamic memory allocation is usually problematic in firmware in general.
- LiamPowell 2y agoSPARK supports both of these things.
- nottorp 2y agoSpark is Ada not Pascal. Pascal strings used to have their actual length in a field at the beginning of the string. Imagine how many off by one errors and how many (even hidden) calls to strlen() that saves. All they needed to modernize Pascal is some library code to resize the buffer if needed, just like curly brace languages. It may already be present in modern Pascal implementations, I haven't followed. Pascal also has array bounds checking by default. Imagine how many out of bounds errors this could prevent. But no, you have to have curly braces instead and build layers and layers of classes and languages over classes, all over the same impractical string representation.
- pjmlp 2y agoObject Pascal and Delphi dialects have had open arrays for ages. And this was even fixed in ISO Extended Pascal by 1990. Not to mention that Wirth fixed this in Modula-2 in 1978, already, which everyone keeps forgeting it was actually designed for systems programming, while Pascal was originally designed in 1972 for teaching programming concepts. But sure enough, lets complain about ISO Pascal from 1976.
- pjmlp 2y agoStuck in 1976 Pascal?
- anta40 2y agoImagine if "we" are OS/embedded dev folks. I mean, for writing userland apps, various langs come and go. But for writing OS, after more than 4 decades, C is still there. :D
- sylware 2y agoIt would mean we need more RISC-V performant hardware. Because the real and honnest way out from C is assembly (with super high level languages with interpreters written in assembly). And it means a worldwide royalty free standard. I guess we could get a middle ground with a simpler C dialect with the bits required for modern hardware architecture programming (no integer promotion, no implicit casts, only sized type, only one loop keyword, no switch...). The defining criteria for this language: it must be easy to get a real-life bootstrap compiler with one dev (reasonable amount of time, effort, etc). I am currently coding many of my applications in RISC-V assembly, with a small interpreter to run them on x86_64, dodging complex macro-preprocessors (I use the basic features of a C preprocessor, I don't even use the RISC-V pseudo-ops). The only thing keeping me on x86_64 are video games for linux and the fact that x86_64 micro-archs are mature, performant wise.
- tehologist 2y agoWhy not just use a verifiable subset of C? https://compcert.org/compcert-C.html https://compcert.org/compcert-C.html
- aeneasmackenzie 2y agoCompcert guarantees that the executable that comes out does what the code that went in said, it doesn’t guarantee much about the code that went in.
- LiamPowell 2y agoThere's also Frama-C, but having used both Frama-C and SPARK I can say I'd pick SPARK any day. Having a rich type system and not having to work with pointers makes proving a program so much easier.
- MaxBarraclough 2y agoRight, Frama-C can formally prove properties of C code. There are also proprietary solutions that do something similar: • https://www.eschertech.com/products/ecv.php https://www.eschertech.com/products/ecv.php • https://www.trust-in-soft.com/ https://www.trust-in-soft.com/
- outside1234 2y agoAnd then they invented their own language with security holes.
- cdevries 2y ago"Beware of bugs in the above code; I have only proved it correct, not tried it." - Donald Knuth
- bdelmas 2y agoIs there really no speed difference between the 2? I can’t find any benchmarks and it’s quite a claim.