What are some good resources to learn to write very reliable/formally verifiable software?
from flavonol@lemmy.world to programming@programming.dev on 16 Feb 15:47
https://lemmy.world/post/25658197

The University of Pennsylvania offers a free series of books called Software Foundations with the following description:

The Software Foundations series is a broad introduction to the mathematical underpinnings of reliable software.

The principal novelty of the series is that every detail is one hundred percent formalized and machine-checked: the entire text of each volume, including the exercises, is literally a “proof script” for the Coq proof assistant.

The series includes Verifiable C, which seems very appealing as a way to avoid some of C’s infamous “footguns.” I haven’t read the series myself, but I might in the future because I like math, logic & programs that do what they’re supposed to do.

Are there any materials that would be good as alternatives or complements to this series?

Edit: Adding the Vercors Wiki to the resources in this thread

#programming

threaded - newest

kata1yst@sh.itjust.works on 16 Feb 16:12 next collapse

The NASA secure coding standards are overbearing, obnoxious, over-engineered, and a huge waste of effort.

But they are absolutely correct and the best guidelines I’m aware of.

standards.nasa.gov/standard/NASA/NASA-HDBK-2203

standards.nasa.gov/standard/NASA/NASA-STD-871913

dev.to/…/10-rules-to-code-like-nasa-applied-to-in…

flavonol@lemmy.world on 16 Feb 16:18 next collapse

The Software Engineering Handbook PDF appears to just be a single page with a broken link on it; is there an archive for the document that’s supposed to be there?

kata1yst@sh.itjust.works on 16 Feb 18:45 next collapse

Sorry about that, I’m seeing the same. Here’s the site linked from the Internet Archive

web.archive.org/web/…/swehb.nasa.gov/

Comment105@lemm.ee on 17 Feb 09:29 collapse

Would this be a consequence of the Project 2025 federal purge?

PokerChips@programming.dev on 17 Feb 11:08 collapse

I was just checking the archives and all captures seem to work that I checked until now. Wondering if they’re moving it to WordPress. /s

Hammerheart@programming.dev on 17 Feb 03:36 collapse

That’s kindeof poetic tbh

tatterdemalion@programming.dev on 16 Feb 20:15 collapse

I definitely cannot get behind the “no recursion” rule. There are plenty of algorithms where the iterative equivalent is significantly harder and less natural. For example, post-order DFS.

I guess maybe when lives depend on it. But they should be testing and fuzzing their code anyway, right?

EDIT: I can’t even find in the NASA PDF where it mentions recursion.

FizzyOrange@programming.dev on 16 Feb 20:49 collapse

You can transform any recursive algorithm into iterative pretty easily though; just create a manual stack.

The rule definitely makes sense in the context of C code running in space. Unbounded recursion always risks stack overflow, and they probably don’t have any tooling to prove stack depth bounds (you totally can do that, but presumably these standards were written in the 1500s).

solrize@lemmy.world on 16 Feb 19:44 next collapse

dwheeler.com has a lot of good links. Also look at learn.adacore.com course in SPARK.

0x0@programming.dev on 17 Feb 14:36 collapse

I was gonna say, if you want formally verifiable, you’d have to go Ada.

tatterdemalion@programming.dev on 16 Feb 20:22 next collapse

I would take a look at LEAN4.

lean-lang.org/functional_programming_in_lean/

FizzyOrange@programming.dev on 16 Feb 20:52 collapse

Yes, but be warned, formal software verification is proper hardcore. Complicated computer science theories, scant documentations - much of which assumes you have a PhD in the field, and in my experience it’s quite a leaky abstraction. You’ll end up needing to know a lot about the actual implementation of Lean to figure out why some things work and others don’t, in a way that you don’t need to in “normal” languages.

It’s quite satisfying when it works though. Like a puzzle.

I highly recommend this fun “game”: adam.math.hhu.de/#/g/leanprover-community/nng4

frankenswine@lemmy.world on 16 Feb 23:30 next collapse

Chris Hobbs write a nice book for the context of embedded devices

___@lemm.ee on 17 Feb 20:50 next collapse

You should look into Coq as it seems to have some good traction.

coq.inria.fr

Mikina@programming.dev on 18 Feb 08:40 collapse

What would be ELI5 use case of this? It has been almost a decade since I did anything math-formal in college, and I wonder what would be some practical uses or situations is SW dev where you should turn to this language.

EDIT: I skimmed the intro to Verifiable C, and I think I vaguely understand the idea - do I get it right, that the point is to basically create a formal definition of the function you are writing, i.e if you have a function that takes an array and sorts it, you’d have something like

For every sequence a and every i, 0 <= i < len(F(a)) -> F(a)~i~ < F(a)~i+1~

(Or whatever would the correct formal definition be, I don’t really remember the details, I know I missed some stuff about properly defining the variables, but the idea of the definition should be kind of correct)

And then you define this formal definiton in CoQ, then somehow convert your code into CoQ code it can accept it as F(a), and CoQ will try to proove formally that the function behavior is correct?

So, it’s basically more robust Unit Testing that’s backed by formal math proofs?

___@lemm.ee on 18 Feb 14:15 collapse

Right, in effect you break down the possible function states along with a more rigorous form of targeted unit testing.

I don’t believe they used coq, but the sel4 Linux kernel is one of the most famous formally verified applications/systems.

github.com/seL4/l4v

The way to beat vulnerabilities is to use formally verified building blocks in my opinion.

paequ2@lemmy.today on 18 Feb 21:37 collapse

Formal methods and TLA+ are a common way of writing verifiable software.