/psst/ - Programming Safe Systems Thread

If there were more spinning blades in the world maybe there would be fewer brainlets.

Attached: 1405725244323.jpg (640x480, 140K)

If Eiffel compiles to C and C is inherently unsafe, how can Eiffel be safe? Can anyone answer that?

dev.eiffel.com/Eiffel_Compilation_Explained
eiffel.org/doc/eiffelstudio/Melting_Ice_Technology

Attached: beaver.jpg (180x279, 7K)

C is not inherently unsafe but people programming in C often design unsafe software. This is typically because they do not understand the issues and the risks. Even for very well informed, it is often too difficult and complicated to design large systems without tools, methodology, support and safe guards.

Attached: bungholio.jpg (1280x720, 78K)

That's basically what he said.

Attached: 1547588229060.jpg (1080x1349, 168K)

Noob

Attached: Viable-Systems-Model.png (494x750, 127K)

Ok that is weird. I posted that exact message a week or so ago but this is not showing as my post and I did NOT post an image.

>C is not inherently unsafe
it is

This is an excellent post.
Concise, well thought, correct.

If you are aware of a discrepancy or ambiguity in the semantics of the C standard, ISO/IEC 9899:2011, or of any C compiler that does not produce machine code that logically represents those semantics, then that would be a big deal and you should come forward with your findings so the problems can be corrected.

Boob

Attached: Venture-Bros-04jfut65b.png (512x384, 300K)

are you a Eiffel shill or something?
jesus...

I () disagree that that's what I said.
And I believe the argument falls apart when you talk about the large scale. C has problems that are at the small scale. There's nothing that makes architecture harder in C. What is harder is having people adhere to the established interfaces.
I find that a double indirection example is. Imagine you have a pointer to a pointer that could be null. It's very easy to write the code that just dereferences the pointer twice. Assuming it not to be null. Could you protect that through interface in C? Not really, the potential for an immediate dereference is still just as prevalent whatever interface you produce. Because you have the pointer and it's operational.
If you instead stored an index you're gonna have to index an array to get to a pointer. There's other benefits to this in certain systems but ignoring those and just looking at the interface what we've got is an additional step that reminds the programmer of the state of their pointer hopefully. You could also have a function that does the indexing and checking if it's valid. It can return a null pointer if it isn't which would give you a crash instead of memory corruption. That's huge. And ideally the function would have exclusive access to the array aswell. We can't really guarantee that but because we've now got another symbol involved we've got an easier time guarding against it by checking how many times the symbol is referenced.

What C lacks is a third process of improvement here. Say we wanted this underlying access pattern. How do you wrap it? You could wrap the index in a type and only expose valid operations. There's countless ways depending on paradigm.

This is kind of a dumb question however, I really want to become a good programmer because I'm really am passionate on it. I already know some C/C++ and I'm currently studying oop on my own. What things you think should I learn more to become better?

Are you new to Jow Forums?

eiffel.org/downloads

Your post suggests your thinking might be a bit cluttered and out of focus. You may also have a context/relevancy problem. Are you on the autistic spectrum?

I've been trying to learn isabelle with the intention of modelling C++ and verifying my shit with it.

It's pretty hard, though. Figuring out why the automated proof methods didn't work and structuring the proofs to get around that is a pretty unfamiliar intellectual challenge to someone used to conventional debugging.

Attached: Isabelle.png (1587x1113, 232K)

Its just late and I'm typing on a phone. Did some odd edits.

And what I was explaining changed while I typed it really. I had set out thinking I was gonna explain a model where you tombstone the target of the indirection. Not just where you null. Ended up doing some dumb mix because phone typing is slow.
That case where you just null is to harmless if you've got sufficient code coverage.

You want to use an automated proof to verify that your code is shit and you are having trouble configuring it all? Hmm, what could be the problem...

>what I was explaining changed while I typed it
Sheesh, dude. Do you operate like that while writing software?

Attached: ADD.jpg (378x550, 34K)

Well, fully automated theorem proving suffers from a combinatorial explosion of complexity. You can do some stuff, like an automatic simplifier but there's limits to what that can do.

So then you must define a series of lemmas to build up the logic of the proof, but knowing what to put in the lemmas so that the simplifier can then solve it is causing my brain to be full of fuck.

Is this some kind of exercise for a class?

No, but the idea of being able to prove my code has none of various common classes of bug gives me a nerdboner.

>do you hold the same standards for your late night kazakhstanian roofing enthusiasts forum posting as you do for your code base?
Of course.
user you just seem stupid when you assume things about people without any regard for circumstances.
Do you do that in real life as well?

Rather than assembling and configuring a hodgepodge of tools and technologies that might have significant incongruities and fundamental limitations, have you looked into any of the complete, coherent systems that were designed for formal verification?

blog.adacore.com/formal-verification-made-easy
"Building High Integrity Applications with SPARK"

Attached: Building High Integrity Applications with SPARK.jpg (334x499, 27K)

ADA/spark is of interest, and I do intend on checking into it. Ultimately, I suspect I'll still have to learn a theorem proving environment, though - Language features like type checking and contracts are typically limited by what kinds of proof the compiler can automatically do without any user assistance. I think you need to go interactive to get the full range of possible proofs.

It's late here, too.

all safety measures are memes. why hang yourself by your own tether? a true samurai is not afraid of death, and neither should his code be. never check or sanitize anything, always assume correctness. the freest and most flexible language (ANSI C) is therefore the ideal.

in his mind, the stack has already overflown, the program has already crashed, and the code is already deleted without a backup. he only awaits the inevitable.

Attached: c5777b1d-53b3-45bd-8f23-729d10075818[1].jpg (494x640, 30K)

The Alt-Ergo, CVC4 and Z3 provers are all installed with SPARK.
Alt-Ergo: alt-ergo.ocamlpro.com
CVC4: cvc4.cs.stanford.edu/web/
Z3: github.com/Z3Prover/z3

docs.adacore.com/spark2014-docs/html/ug/gnatprove_by_example/manual_proof.html

youtube.com/watch?v=VFp0mYdF6nc

Attached: 1138px-David_Teniers_(II)_-_Twelfth-night_(The_King_Drinks)_-_WGA22083.jpg (1138x900, 233K)

Cool. Will definitely look into that.

The productive work is going on in Coq. Checkout these books:
softwarefoundations.cis.upenn.edu/
and this crazy project: vst.cs.princeton.edu/veric/

There is a long, hard road between an academic project and an engineering tool.

SeL4 wasn't productive?
One of the problems I'm having getting into this stuff is there doesn't seem to be a clear consensus about what system is better for what.
I mean, for programming you'd probably use python for new learners or quick and dirty stuff, then migrate to something like C++ once the system gets large enough. Can't really find any such consensus for formal verification..

Yeah, sadly yeah. But it does things no engineering tool does, like allowing recursive predicates, and it does it with actual C and with an actual compiler, so it's not a typical academic project, either. But yeah, not an engineering tool... yet

SeL4 was super productive, but it's from a prior generation. Their methodology hasn't extended to other problems; it was bespoke by design.

Might also checkout
youtube.com/watch?v=ZcT49NAU-4U

Dude does a pretty good walk through of the stuff they've been doing in Coq. What's blowing my mind is that they're actually doing real systems.

My whole career, formal verification == toys or super special cases. The last 8 years have really turned that around, though.

The tools are still shit and still take years to master, though. That hasn't changed.

Awesome. watching that now.

how 2 write safe javascript?

Software Synthesis? youtube.com/watch?v=omsuTsOmvsc