So my professor for this programming languages class i'm taking in college told us that Rust is a superior language to...

I wanted to learn Rust as my first language and it totally kicked my ass. I picked up Go instead

they does

Found the tranny

Rust is simpler for beginners point of view. The compiler toolchain is simpler to set up and doesn't have weird quirks on every fucking system (especially windows). There are tons of human-friendly features that C could have, but the language is written in stone since 90s and was meant to run on 90s toasters and was shaped to that. It's not that Rust would be great, its just that C is so bad.
As for the language itself, I don't believe in owned pointers. The language just pushed so many things that make the compiler and language specs too complex. It's not a direction I would love to go.
Don't worry too much about what you are taught in college. You are just provided some guided way until you start to understand things on your own. It's normal to learn multiple languages. And then language doesn't matter _that_ much.

>LGBTQ+ are people too
They literally aren't. Your parents must have done a shitty job raising you.

What's wrong with you psychos? These are people who show uniqueness, healthy bodies that have reached the top of the Maslow pyramid and can serve as an example of freedom. Freedom from prejudice, freedom from traditionalism (and nationalism), freedom from archaic chest-beating. Were you all raised in absent-father families (sorry if you were)?

i think you misinterpreted that picture

Attached: 0BAD98F3-3889-42AC-89AA-F7D8282EEDAD.jpg (884x728, 85K)

I think you need to go dilate, sweetie. Wouldn't want to let your festering axe-wound close up, would you?

What axe wound? You are living in make-believe.

nobody fucking reply to this baiter

Use Ada/SPARK, which is the language to use when bugs would make things go boom.

Rust is the greatest language ever designed. Even if you won't use it daily, just understanding it will put you above 95% of developers

Rust deprecated C++ which deprecated C
Therefore Rust deprecates C as well.

>Ada/Spark
hownot2code.com/2016/09/02/a-space-error-370-million-for-an-integer-overflow/
has costs tax payers $370, 000, 000.

Rust has a decade track record of being safe.

We use TLA+ now honey

There is no good framework to make GUI applications in Rust, you'll have to use bindings.
That's why companies use C++, it's just superior to make UIs with Qt.

Just learn C#/.NET. Learning esoteric / low-level stuff like C and Rust is a complete waste of time in today's world--if you want a real job, that is.

C will always dominate embedded programming.
Linux kernel development will always be C too for the most part.

Yeah. uhhhh. You can use C++ code in rust.

Because nobody uses it since it's only one decade old.

There is no reason for C to dominate embedded. Rust and C++ compile to machine code and C++ is used on planes and such.
>Linux
was written 30 years ago and is mostly legacy code. The idiots won't accept modern complementary languages.

My point still stands. Ada has a bad track record, Rust doesn't. Lockheed switched to C/C++ over Ada. That speaks volumes for the F-35. It's only a matter of time before they use Rust once Rust gets a certified compiler.

Why would they use Rust, what logic analysis tools does Rust employ?

>My point still stands.
>don't have a bad track record because nobody fricking uses it
Good point m8, that's a very big brain that you have

Not an argument, really.

BC. Rust is a huge improvement in memory safety that no other language has. Not even Ada. Not to mention Rust is 1.9x faster than Ada. It's even faster than C/C++ if you're looking for consistency.

Attached: file.png (680x381, 86K)

What if there's no C++ or Rust compiler for the said embedded device, you dummy dum dum?

C++ has the backing of GCC which can run on basically everything.
Rust has LLVM which is getting there as well. Once rust has a GCC frontend it's over.

When you make a deal, you know what components you're buying.

Read your own article. They incorrectly reused code from the Ariane 4. Ada is just a language, not an AI. In fact, it's the only language besides SML that actually bothers to take finite precision arithmetic seriously, meaning give the the correct result or throw an exception, while all the rest force you to use modular arithmetic or God help us, makes signed overflow undefined behavior.

That has nothing to do with logic analysis..... In what way is rust competitive to SPARK and TLA+

Wouldn't have happened in Rust. Rust doesn't crash on a simple overflow @ opt_level=3
Rust is faster and memory safe, you can't say the same about Ada and SPARK is literally a toy language used no where. SPARK 2020 even is planning to split from Ada again ruining the one good thing SPARK had going for it.

Dude I can eliminate 99% of memory unsafety in C++ by converting the entire codebase to smart pointers, gsl::not_null, gsl::owner etc. It's just a standard library addition away.
What I want to know is, how do I emulate the SPARK experience where I write logic behind the scenes so my code gets automatically audited/proven?

>rust professor
>in college
wtf? what kind of college is this?

Attached: JMqtv.jpg (400x300, 22K)

All colleges have extracurriculars...

>Wouldn't have happened in Rust. Rust doesn't crash on a simple overflow @ opt_level=3

Last time I checked Rust panics on overflow in debug mode compiles and just wraps in release mode, which is hilarious. Good luck with that, maybe the rocket would do a Immelmann turn!

>>rust professor
OP didn't say rust professor user.

This fucking example again.
The used the wrong config for the accelerometer -> Value went over defined range. Defined range was, by design, already bigger than acceptable values. -> Computer rightfully interpretes the rocket is going awok -> rather than letting fall into a city (the sp called chinese style) rocket explodes.
The computer (and the language) behaved as expected.

C is still used in embedded which is a huge industry. Rust is decidedly terrible as an embedded programming language.

It may be a superior replacement to C++ for quite a few applications but only time will really tell.

Hey switched to C++ because they believe is cheaper to find codemonkeys than to form them, everyone expert in the field agrees that it is a step backwards

>converting the entire codebase to smart pointers, gsl::not_null, gsl::owner etc.
All of which Rust gives you for free, and in most cases without any runtime cost.

That's exactly the reason, and that's why software "engineering" is becoming such a fucking joke.

So? Can you answer the other question?

It's the same when, in the end, they will run at the same speed. The only difference is that the C programmer has to know what he is doing more than the Rust programmer. Using unsafe code blocks in Rust is essentially writing C with different syntax as C is just a minimal abstraction over Assembly compared to modern high level languages. Rust program will run faster than badly written C but at the same speed as well written C. The difference between compiled languages is essentially the syntax and the features they provide. Rust is technically superior as it provides the ease without losing speed, but the end result of good C and good Rust is the same. One is just harder to achieve than the other.

AFAIK, this currently isn't possible with Rust.

>Cniles defending Ada
pathetic.

Weeeelll darn! That means we stick to ADA/SPARK. Nice try Rust.

I really want to take on rust with an open mind, but comments like the one of this retard keep me far from the language

>it wouldn't have happened in rust
Then you would have a 150 ton bomb travelling at several km/s with no fucking idea of where it is going

it's pretty rare to need to use unsafe blocks, but even if you have a need for it it's good maintenance and debugging-wise to have potential problem areas explicitly marked

There's an extremely good chance it would have gone into space.

>What I want to know is, how do I emulate the SPARK experience where I write logic behind the scenes so my code gets automatically audited/proven?
Use C until Frama-C does modern C++ (never, because you can't really hire white people for academic positions anymore in F).

Based Microsoft has the fewest trannies. It feels like sjws are attracted to anarchy

>C is just a minimal abstraction over Assembly compared to modern high level languages
it would be easier if C were just this, but it isn't. aliasing, alignment, and vectorization prevent you from treating it like that on modern systems.

ironically its C++ that will eventually replace C in embedded. it's really the platform providers dragging their heels on C++ support which has preventing the adoption of an embedded subset of C++ from being used.

Rust deprecates C++

TLA+ isn't a programming language, it's only for verifying specifications
SPARK is an abomination to use for most tasks

For some tasks, but not all. Rust lacks many of the meta programming and compile time programming features of C++.

Reading fast about SPARK, it's about automatically generating tests?
Looks really cool, I wonder why so many require a human to write them.
But if those contracts are required for every function...? Might as well write tests with the same effort.

You're right, Rust lacks the shitty parts of C++.

No, most of the C++ applications have a GUI and Rust doesn't have good frameworks for making UIs.

You are confused, the difficult stuff is to put things in space. An example:

en.m.wikipedia.org/wiki/Intelsat_708

m.youtube.com/watch?v=VewiLEXQnYs

Unit tests don't 100% prove correctness unless you take the time to verify all possible cases, which I doubt you or most programmers do. They try to aim for as much as they can until they feel good about it.

SPARK removes that and automatically proves your function based off simple pre/post conditions. I don't know why you would ever want to write tons of test cases over letting a computer prove your function for you.

SPARK is about mandating a formally verifiable interface for programs. It requires every function have a well defined specification for valid inputs and outputs.
It's about more than just writing tests. Tests can only test the specific cases you provide. Formal verification requires mathematically proving that a program will never output an invalid result or enter an invalid state. It is a much stronger guarantee than unit testing can provide.

>Don't worry too much about what you are taught in college
This. Especially which technologies. Those things change all the fucking time anyway.

>>it would be easier if C were just this, but it isn't. aliasing, alignment, and vectorization prevent you from treating it like that on modern systems.
While I agree, that's still minimal compared to other languages.

fuck off with your good advice, i'm only here to display my superiority by shitting on languages and software that I haven't ever used before

The problem is that the expectation doesn't match the reality with C. You would naively expect C to behave in a certain way because it is low level, but when it doesn't it is very surprising and painful to debug.
This expectation doesn't exist in higher level languages, so these mistakes are much harder or impossible to make accidentally.

>not mastering every programming language that exists
languagelet
kek

How would SPARK prove it if it's not just auto generating a ton of different inputs/tests?
Could be a fuzzy generator that tests a function for all kinds of values. How does it differ?

Well, that's one of the skills needed for C I suppose. Which language would you choose for minimal abstraction over assembly while still remaining high level?

Retarded much? Weakest precondition.
Tests don't do shit. This is formal, and actually proves that your function implements the spec you wrote.

The absolute state of rust fags. "Buh it's the best, even better than SPARK, even though I can't even imagine the degree of complexity formal verification implies"
Take a look at "formal verification" faggot.

This is it, I'm out

Attached: 1563931076528.png (400x504, 323K)

That's what I am looking at and searching. What I come to is "This is how you run the verif tool! It works! Just trust us!"

I looked into "formal verification"
>Usually this consists of exploring all states and transitions in the model
So brute force every possible input
>Another approach is deductive verification.
So generating inputs that would be likely to break it

wtf? This is literally fuzzy generator.
I want some practical knowledge. Not some 10 page theories.

Have you taken a math course past Calc? Just curious. Formal verification has nothing to do with testing every single input. You use math to prove that no such input can exist to violate your conditions. This isn't some kind of voodoo shit, it's literally theoretical mathematics.

Just like in mathematics you have basic axioms that hold true and you can use them to deduce other theorems for correctness or in the case of computers algorithms.

>How would you feel if they overtly biased against incels, loners, and spergs?
Have sex incel

Its maths, retard. Supose 2 funcions, one can take values 1 - 100 and the second one, called from the first, 1-10. Formal verification role is to find and demostrate that the first function being called correctly will never call the second one with a wrong input. Btw the theory behind is fucking thicc and a little more complex than brute forcing

Deductive verification is not generating any inputs you subhuman 80IQ trash.
It (extremely oversimplified) translates your specification into proof obligations, and your program into logical formula, then asks some prover "SAT?".
This is nothing like enumeration techniques. It proves _every_ possible input produces output that is correct wrt. specification. Not that a set of given inputs produce outputs deemed correct by someone writing the test, on given muchine, in given run.

Anons went off course and blew off steam. If you're still interested, take a look at Introduction to Algorithms, the algorithm analysis part. You assign a collection (may be empty) of predicates to each line of code in your program and specify which lines of code they encompass while still being correct. This is called an invariant, you are aiming to prove that, for instance, a for loop that increments each member of the array is not off by one index or more.
Now what uses predicates? Logic programming. You want to program logic. So you write your original C++/etc source code and parallel to that write the logic which sets your invariants. The latter in term is simulated by a logic programming language to check if the final output is truth or false "correctness or incorrectness".
I'm being overly general but go and read some pages, it's very interesting. Keep in mind almost 0 software you use has gone through such a treatment. People generally write code, take a second/third/nth look and simply publish it. Some bundle tests which are nothing more than asserts and exceptions for 0.00001% or less of possible machine states.

homepages.uc.edu/~martinj/Symbolic_Logic/341 Syllabus, Textbook, Handouts, Notes/LPL textbook.pdf
Here you go, it's an introductory book to teach you about how you can prove things without tests. Proving tools are nothing more than just advanced shit from this.

Yeah I see. Amazing that machines can derive functions for logic functions. I wonder why can't see it in other languages if SPARK has such a simple interface for that?
Maybe just not so much logic programming?

Didn't do much theorical maths, just a few proofs in group theory. Didn't care for more as I wanted to code stuff.

I'll take a look at those links

There's a few languages that can do it actually. Most are FP languages though which makes things waaaaay easier. SPARK is a subset of Ada and there are things removed that would otherwise make proving hard (like pointers). Although the next iteration of SPARK is bringing back pointers (blog.adacore.com/using-pointers-in-spark) to a limited extent that's provable thanks to work in Parasail and Rust.

>There is no reason for C to dominate embedded
t. never wrote embedded code

>I wonder why can't see it in other languages
We can. There's Jessie for C and Krakatoa for Java. Biggest issue for deductive verification is most languages are implementation-specified which is pretty much equal as being unspecified.

Because what people today consider elite schools of coding, programmers of 40s-70s did on paper and punchcards, without redos. It's the natural progression that we go from programming as a freedom, as a pastime, as a recreational learning tool, to a much more serious and professional attitude.
I'm a mathematician myself though I can safely say I program C++ better than average; specialise in logic and optimisation. I can recommend you read the entire CLRS if you haven't. Also Introduction to Mathematical Logic and some beginner Prolog programming. Lisp is good but this is pure gold. Mercury is a Prolog dialect that compiles to C, assembly, or directly to machine code with all optimisations.
Imagine, a language where you tell the computer some hard facts, some other facts that these facts imply (via predicates), and then ask whether an arbitrary predicate of your choosing is true or false. Fantastic and lambda-complete. It really is like speaking to artificial intelligence.
Here, my github.
this_is_a_fact(var1, var2, var).
implied_by(var) :- predicate_1(), predicate_2(), ... //, = AND

github.com/PeterBadzhakov/Prolog

Dilate

Evergreen...

Oh I see. Many languages just give you unit and integration tests and don't mention this. In non-logic programming it's not as much use is probably why?

Thanks. I'll take a look at Prolog and reading the Introduction to Algorithms.

A lot of this stuff is really theoretical and my lazy mind gets bored. I'll make progress slowly..

Good to see that you are ready to accept that there is more than the shit rust shills keep vomiting everywhere.
Formal verification is a very difficult and well payed field user. Good luck

You can directly apply logic to a piece of code right now. You can literally watch a video about prolog and understand the whole language in 7 minutes.
For instance:
>John is Marie's father
>Jack is John's father
>grandfather is a father of someone who is in term a father of someone.
>Who is Marie's grandfather?
X = Jack.
> true

Congratulations, I just taught you prolog. That's all the syntax there is in this language.

Oops, parent() must be father()