What is the best language for safety-critical applications?

What is the best language for safety-critical applications?

Other urls found in this thread:

en.wikipedia.org/wiki/SPARK_(programming_language)
youtube.com/watch?v=QIrpi8_1P9g
stroustrup.com/JSF-AV-rules.pdf
github.com/rust-lang/rust/issues/29723
github.com/rust-lang/rust/issues/41646
blog.rust-lang.org/2014/10/30/Stability.html
github.com/thepowersgang/mrustc
adaic.org/learn/materials/
adapower.com/index.php?Command=Class&ClassID=FAQ&CID=328
muen.sk/
en.wikipedia.org/wiki/Racket_(programming_language)
gnu.org/fun/jokes/unix-hoax.html
twitter.com/NSFWRedditVideo

Ada
(Enjoy a Rust-Free first post™)

Give an example you faggot.

/thread

Airplanes, satellites, missiles, bombs.


wew lad it's like you're not even trying

It's like you cannot read. Since you did not define saftey-critical in your lazy OP, you cannot expect a highly specific answer. There is a subset of Ada called Spark which is along the lines of what you're looking for.
en.wikipedia.org/wiki/SPARK_(programming_language)

However, since you a clearly a retarded nigger, I suggest you stay far away from programming any critical infrastructure. Consider web programming.

Rust, ada, or pascel. This tbh though.

haskell

Coq

Have you considered rewriting Ada in Rust?

Rust is 105% safe you could use it for government secrets and nuclear bombs

Can someone explain why rust is suddenly hated here? there wasn't this many anti-rust shills here 8-9 months ago.

4pleb exodus combined with finding a compiler error for rust that destroys memory safety, and that still hasn't been fixed in eight months.

tranny sjw code of concucks

People are tired of the Rust shills. Nobody actually uses Rust except the shills.

Well, C is provably the worst language, and the irony that it's fairly entrenched there is more or less by accident.

Probably Ada running on one of the Green Hills systems tbh.

That's exactly what Ada/SPARK is used for and is the best at.
youtube.com/watch?v=QIrpi8_1P9g

C

I read that they used C++ in the F-35 JSF. Then I read how the airplane shows duplicates of the targets when networking with friendlies, confusing the pilots to the point that they don't know what is really there and what isn't.

So Ada.

...

Did you know they had a big-ass coding style manual that Stroustrup himself hosts on his personal page? And the pros still fucked up?

stroustrup.com/JSF-AV-rules.pdf

They're not "pros" if they make something that broken and think it's fit to be put into actual airplanes before they catch any of the problems.

The safest language is the most reviewable language, especially by non-experts in the language (who may be domain experts, instead). So, not fucking Haskell. Not even C++. Ever.

But to immediately contradict myself, it's clear that code can be deliberately written for reviewability. You can separate code into stateless bit-twiddling functions (ideal reviewer: another programmer; automated testing) and then have all of your domain logic in its own section (ideal reviewer: guy who know how planes work). I've done this in Perl of all languages. One reviewer certifies that the functions do what the text on the tin says they do. Another reviewer certifies that the logical operations won't result in Chernobyl.

A key component is making it easy to follow errors as well. What happens if there's an error in this part of the program, vs. an error in this part, ten lines down? Early on in an operation it's probably good enough to abort, release control. Later in an operation you may have to stabilize a piece of heavy equipment first.

Disclaimer: I have no idea what actually happens with safety critical industries. I imagine it's done very badly, and that safety is probably handled with cargo-cult decisions. "I heard that banks use APL and ML. And you know, those guys are serious."

Aaaaand checkmate. C++ lacks features to prove the absence of runtime errors, various levels of correctness, etc.

Terry Davis did this type of work with C and ASM.
If you weren't a larping faggit you could do the same w/o crying for a handicapped language.

I'm quite sure it was already well hated 8-9 months ago. In fact, I don't think I cannot remember a time were rust was ever celebrated here.

It seems to me that you're trying to rewrite history to make it seem rust are oldies and haters are newfags or wathever.

People hate it because of the CuC.


That position is untennable as a channer. Get out.

Rust users are erratic and liars, they talk about safety as the most important thing but they wouldn't be using their language if that was the issue.
When pressed against the wall they themselves erect with their own contradictory arguments they begin insulting, trying to force meme about missiles and suggesting people to "kys".

and those are????

...

do you mean this? github.com/rust-lang/rust/issues/29723
if so, this was not neglected and it will be fixed soon

github.com/rust-lang/rust/issues/41646

anyways if you dont want to be a #rustmissile that is fine. just kys instead

It's a meme that everyone here likes Rust. While Rust might have some upsides, the fact of the matter is that not everyone enjoys the Rust shilling that has recently infected the board.

i have been shilling rust on Holla Forums for more than a year now

Not just that. I for one hate it because it's an inferior language. No subtyping, no contracts, shitty way of handling number overflows, unreadable syntax, and its only claim to fame is a clunky poorly implemented Yet Another Way of ensuring memory safety. It's a pile of trash that wouldn't get the time of day from the industry if it wasn't for SJWfaggots pushing it.

what is your problem with it?

It doesn't report errors and is tied to specific hardware. So shitty both from a safety perspective and an embedded perspective.

it isnt tied to specific hardware though.
also you can pass -C overflow-checks=yes to rustc.

Last I checked it the language standard was to silently apply 2's complement wrapping. Hence specific hardware. But oh, silly me, forgot that Rust doesn't even have a standard either. :^)

nothing silent about writing it into the spec
hardware that doesnt use two's complement can emulate it.
nice >muh spec meme. please look up how long it took for c/c++ to get standardized.

also please tell me what rust should do instead.

Fork, remove CoC,
SJW leave offended, thus making unuseful to leave, language might or might not be better with time.

SJW are also prone to government cooperation if it's for the sake of "diversity", cronysm or "dismantling capitalism", another reason you don't want them near any "safety" effort.

wtf are you babbling about? we were talking about integer overflow and then you autistically screech about cocs, sjws and diversity?????????????

Why should I care about those festering piles of shit? Why don't *you* look up how long it took Ada to get standardized.
Overflow is an error condition. That error should be reported in all cases. But this ties into Rust using return value types rather than exceptions for error reporting, which would make reporting such a thing clunky.

why dont you tell me why rust not being standardized is bad?

see
if you dont want it to panic, use the checked_* functions

execeptions are cancer though.

Nah, you asked what rust should do. Rust should drop the CoC.

You will not even get uninterrupted a suggestion of how rust could do things better.

You shouldn't get help even if you crawl outside of your safe space. If you want to use rust, fix it or return with your friends.

about integer overflow

You got me. I should've said "Rust doesn't even have a spec" since that's what I'm really complaining about. There is no complete, stable reference definition for the language. That is bad for stability, adoption, predictability, etc.

none of those reasons have anything to do with not having a complete specification though.

no stable definition -> no assurance of a particular feature sticking around long term
no complete definition -> "what happens if I do this?" "I dunno, doesn't say, guess you'll have to poke about and try it and hope it's not implementation-specific"
no stable/complete definition -> fewer implementations, more fragmentation of implementations, potential adoption hinderance

but you get agile development

HA HA HA HA HA HA HA

blog.rust-lang.org/2014/10/30/Stability.html
there is no reason to use any other compiler than rustc though
github.com/thepowersgang/mrustc

I'll admit that I wasn't really active during the presidential campaign. I had better things to shitpost about.

go back to >>>/klumpffpol/

You assume that I'm a Holla Forumsack, and attack me based on the way I format my posts to try and shut me up?

I should've been more proactive when the "go back to Holla Forums" posts first started.

That's not how errors work. Rust leaving these errors up to the programmer makes it an unsafe language with overflows.

who are you quoting?

your >>>/the_plonald/ is showing

Has Terry launched any real hardware besides ticket cutters or does he just larp as a rocket scientist in his 8 bit TempleOS video game because he implemented a physics algorithm from stack overflow

I thought this language was purely a Holla Forums meme.

I am sure there is some Holla Forums appeal because the language is relatively obscure, but it is taken very seriously for safety critical applications. It deserves to be more widely known, but I'm glad it has not reached fad status.

You thought a language designed by the US DoD to eliminate as many sources of runtime errors as possible and that is used in aerospace, infrastructure, and the military was just a Holla Forums meme?


It's unlikely to ever reach fad status. Too old and has had too much FUD thrown at it from butthurt C devs.

What about for normalfags who don't have the military's budget to spend on a Spark license? Rust?

lolno

Ada and SPARK are both GPL licensed via GCC. The Ada ISO standard is even freely available, which is unusual for such things. If you don't have the tons'o'monies for a support contract then you just don't get the support. You still get the compiler, tools, annotated reference manual, etc.

What triggers my autism about Ada is that it's case-insensitive. What's a good Ada book? I have Programming in Ada 2012, but is there something better?

adaic.org/learn/materials/
If you've already gone through a lot of the Programming in Ada 2012 book then I'd recommend programming something and referring to the reference manual as needed. I suppose Building High Integrity Applications with SPARK might be of interest.

t. LARPer
you could at least spend a minute to read the wikipedia article about what you're going to larp about

The people surrounding it are disgusting valley trash. Those people attract a crowd of meta-degenerates (i.e. most anyone who utters the word "rust" on this board) like flies feeding on shit. It's like a nucleus surrounded by several electron shells of subhuman beta orbiters.

How many rockets have fallen out of the sky from buffer over runs? Zero.

But Ariane 5 fell due to an integer overflow, and that was written in Ada.

Get some fresher FUD, faggot.
adapower.com/index.php?Command=Class&ClassID=FAQ&CID=328

And this is why you don't hire Pajeet to program your rockets.

A way to reduce the possibility of such reuse-without-checking-spec mistakes from going through in the future is programming by contract. Make the spec assumptions part of the code. That way it can be checked automatically rather than relying on later programmers to do it. Contracts are a feature of Ada 2012 and every version of SPARK from the beginning in 83.

There is no 'best' language for high reliability systems, there are only best practices. Best practices being formal proofs, which 99.9999% of coders are too lazy to do.

The only actually correct operating system is seL4, which is writen in C.

There are three issues with that statement:
- It was specified/written in Isabelle/HOL and translated/implemented to C, which is very different from just writing it in C.
- Muen exists: muen.sk/
- An operating system is not merely a kernel. Get your terminology straight.

Probably has something to do with most coders using languages that make formal proofs unnecessarily difficult.

Yea I don't know why I called it an OS when I know it's just a kernel.

The seL4 debs don't actually write the formal proofs first, they write C first which allows them to experimenter with how they want to implement the desired functionality. Then once they have an implementation in C they write the formal proofs for the functionality which are used to verify the code behaves as intended under all circumstances. It works quite well and the formal verification step often picks up undesirable edge cases on the code.

As for languages and their compatibility with formal methods you are correct in that some languages are more compatible that others but to be honest you shouldn't be writing high reliability systems in things like Java or Python in the first place.

I suspect that if you asked people about the worst languages ever created you'd get a good number of people debating M v Ada. I understand what M offers (at a very high price) I've never understood what Ada offers. One of the 5 smartest people I've ever known hated Ada with an unmatched passion. I actual read something suggesting Ada was designed during the cold war as a misdirection campaign for 2nd world spies.

1) High reliability/safety-critical systems don't rely on software to provide these qualities.
2) If they do, the software should be as simple as possible: Assembly, hopefully on a separate chip. Your main, more complex application (the ones you write in a higher level language for a general cumputer) should be separated from this.

Ada/SPARK is designed to provide syntax and a compiler without assumptions to provide deterministic behaviour for your software. However in the most cases the weakest link is the programmer himself, and picking a easier functional language is better,

Garbage collection pauses rule those out. Functional languages characteristically have runtime profiles which are hard to predict.


I suspect you'd hear PHP, Ada isn't known well enough for people to debate. The rest of your post is too silly to respond to.

en.wikipedia.org/wiki/Racket_(programming_language)

You're a poor African in a remote village and there are 5 white people who sometimes visit your village to fix the computers in your community center. Do I have that right?

what the fuck am I reading…

this is horse shit

yes you are

...

You got it friendo. Have you ever thought it is just so great that everyone who starts using it also evangelizes it?
Now you do. Come to us matey, and soon you will be shilling the best language ever.

Serious answer to OP, use coq. Proof is the best way for safety critical uses, don't say I didn't tell you.

javascript

Prove ME wrong

"protip. you cant!"

Microsoft BASIC on CP/M tbh fam.

Thanks. I haven't read much of Programming in Ada 2012 yet, only the foreword and the part where it says that Ada is case-insensitive. It hasn't made me want to throw Ada out of the window of course, but it left a weird taste. Common Lisp does the same thing as well.

I'm not claiming to be the smarterest, but I hate Rust with a burning passion because working with it is ass backwards, not because the resulting products are bad. Basically, it's good when others do it like CSS. Your post is all sorts of dumb thom

Case insensitive is a good thing when you program the huge systems done with Ada over a narrow (semantic) field.
I'm bored of seeing again and again people naming their variables of functions similarly, and I have seen many times problems in C because people wrote the same function with or without uppercase.

Programming guidelines and namespaces help with this problem, but the point of Ada is to assume that the programmer is retarded anyway, and to avoid as many errors as possible derived from this fact.

People telling that C or C++ with guidelines are as safe as Ada/SPARK in this thread have no idea of what they are speaking. Even in those cases you really need all kind of static analyzers and compile flags for run-time checks that basically try to imitate what Ada does by default.

The key of safety is to limit human mistakes to a minimum.

Yeah, lazy evaluation in a safety-critical system! Just kill me already.

t. LARPer

there is, if you wanted to have a coc-less implementation this would be really important.

I don't need to know about your meme language.

Apart from education and very specific problems is useless. Saying you can create something like the control system of a plane with it is high quality autism.

...

What the fuck are you taking about?

why did you put a space after the >> line?

I make my own computers and programing languages. Holla Forums is a lazy ass reddit user.

He conceded that he lost the argument, so he screamed about your line spacing and ran away.

ok

Even with strict Haskell, you still have the unpredictability of garbage collection pauses, so it really depends on the realtime requirements of a critical system (some further break this down into hard/soft realtime systems).

navajo

actual non-larper here.

C is the answer for highly safety-critical applications. written for lots'o'loonixes (including famous qnx). most severe industrial (mining facilities) specifications. all passed by every reviewer possible, all certificates granted.
In reality (and not in your larping fantasy) most of the time most robust hardware (i'm not even talking about client-side software!) fails. And when it fails, it fails miserably, so watchdogs and hardware-based exception interrupts are implemented.

If you wanna continue larp about "muh PGP", remember: all your logs belong to isp, means to cia-niggers.

Why would you go on the internet and tell lies, user?

I've done safety-critical work before and we used C. I can't imagine doing safety-critical work in a language where the working set size is practically random.

And I can't imagine doing safety-critical work in such a ridiculously bug-prone language. Well, actually I can, but I'd want to run far far away afterwards unless formal correctness proofs were involved. You did safety-critical work *despite* C. Ada/SPARK completely blows it out of the water in every way possible, no contest.

Another user working in critical software.
Both of you are right. Ada/SPARK is better, but lot of C code is used.
For example, satellites is historically a C business, while rockets is Ada (for some reason).
It also happens that until 4 years ago Matlab had verified C and Fortran transcompilers, but not Ada. That stopped A LOT of people (phisics and mathematicians) in aeronautics and space to use Ada. Luckily that has changed and Ada2012 is looking strong.

Funny fact: the f35 is the first plane in a fuckton of years programmed in C, instead of Ada. It was a clever move to save money as there are more (and cheaper) C developers than Ada developers. That went fucking well, as we all know.

Where are my God damned hovercars.

I thought it was just a meme?

Navajo

Why are you surprised planes's are running computer software???

< modern day Holla Forums
< t. non-larper

modern day kids would never imagine that their coffee machine runs on a (AT LEAST) 8-bit 8 MHz MCU, which is comparable (if not superior in every way, except for pajeet programming; Lord! Save us from python (to strict-C, ofc) translators!) in terms of speed, registers, peripheral e.t.c. to famous F-14 20-bit MCU.

Someone wanted real answers? It doesn't really matter which language you use, it only matters how easy it is to read and understand flaws and unintentional errors in your code. You may go full retard and pretend like "Forth" is the future (when in reality it's just a bloated assembler with its own LLVM), Java "owns" (no it's not) or another trend-of-the-day meme language (you sound like a bloody SJW, but PJW). At the end of the day people who do work use ANSI C, Assembler (for crucial speed improvements, specifically using modern MCUs with FPUs to do some DSP), VHDL, STEP7 Now i also heard about ADA, but 've never seen anyone actually using it, even managed to see Fortran, Cobol, Pascal old fucks, but most of them are gone now.

If you are fresh from college, or didn't even started (like 98% of Holla Forums) then you're free to larp about it, nut as soon as you hit the real industry you will either switch to the most commonly used language at this company or walk away. If you are supreme master, you may even force them adapting to your language of choice, but you MUST have some real skill behind your back, or they are simply desperate. Also, a good sign company is falling into the ground is lack of strong counter-reaction on your remarks about "their bad choice of software".

TLDR: Want to get into the real industry? Learn the industry way, never listen to some edgy lone furfags who never ever done anything with their hands in their entire lives. Internet was a mistake

Even when I was working for a defense contractor I never saw Ada.

you're trying to hard, faggot

what did you see?

You're probably thinking of this gem.
gnu.org/fun/jokes/unix-hoax.html

Then Dennis and Brian worked on a truly warped
version of Pascal, called 'A'. When we found others were actually
trying to create real programs with A, we quickly added additional
cryptic features and evolved into B, BCPL and finally C. We stopped
when we got a clean compile on the following syntax:

for(;P("\n"),R--;P("|"))for(e=C;e--;P("_"+(*u++/8)%2))P("| "+(*u/4)%2);

To think that modern programmers would try to use a language that
allowed such a statement was beyond our comprehension! We actually
thought of selling this to the Soviets to set their computer science
progress back 20 or more years.

C and C++. It was a 'smart weapons' project based on NT (this was almost 20 years ago).

I read a hacker news post that suggested all the big aerospace, healthcare, and other developers of safety-critical software were diving headlong into Rust for everything.
This was in a thread on something Rust related. I think he was lying since it's been over a year and I haven't heard anything since.

Those industries are extremely conservative with tech and there is no way they would be early adopters of Rust. Regardless of the merits of Rust, they intentionally stay 15 years behind the curve so it's like it doesn't exist.
To give you some perspective, I used to work in healthcare tech and still have a foot in and I can tell you that there was a lot of panic about Novell NetWare ending support this year. Yes, that Novell NetWare. From before you were born. That they were still shipping on devices. Remember online vidya in the distant past before internet was popular where you had to set up an IPX network? Healthcare still churns out IPX devices.

Java

C with the B-method. It's been used in several cases in subways and airplanes when the devs didn't want to risk anything. There's an IDE made for programming with this method (Atelier B). It might be compatible with other languages than C and Ada, but I don't really know.

Not sure, to be honest.
But it wouldn't surpsise me if he actually wrote programs to manage something in space, since he actually is a kernel developer. For Ticketmaster he did stuff for embedded stuff.

assembly

you can't trust anything else

i write rust in binary with a soldering iron i grip with my asshole like lady ada lovelace did in 1830 tbh, its the only way to be sure i'm checking my privilege tbh

Plus TDD right?

Otherwise all that soldering goes into the trash.

wtf are you telling me i incurred 3rd degree burns to my asshole writing rust and it was all for nothing?