codeball-action VS l4v

I found this neat application that finds bugs in your Pull Requests and lets you ship faster and with higher confidence.

Code authoring might be a bit too much to ask of current tools for now, but code review (example 1, example 2) seems much more feasible right now. If employed judiciously it's another effective analysis tool to automatically find bugs, automating a task that can be a tedious challenge for many programmers. A human reviewer might ultimately still need to be involved, but less intensely.

Codeball is a new and ballsy attempt at taking automation further. It simulates the developer intuition and approves safe pull requests, saving teams time.

> Does sel4 have a style checker and/or proof checker that you can run on your c code?

The specification and proofs are open-source [0], but I suspect that they are tailored for seL4-related uses and probably aren't well-suited for "general-purpose" C code. I think using their proofs would also necessitate writing a specification for your own code which is probably going to be an ordeal in and of itself.

They do have a style guide [1] as well, but that's just a small part of the full verification process (described in [2]).

[0]: https://github.com/seL4/l4v

[1]: https://docs.sel4.systems/processes/style-guide.html#verific...

[2]: https://trustworthy.systems/publications/nicta_full_text/737...

> C/C++ can be made memory safe

.. but it's much harder to prove your work is memory safe. sel4 is memory safe C, for example. The safety is achieved by a large external theorem prover and a synced copy written in Haskell. https://github.com/seL4/l4v

Typechecks are form of proof. It's easier to write provably safe Rust than provably safe C because the proofs and checker are integrated.

You can't really retrofit safety to C. The best that can be achieved is sel4, which while it is written in C has a separate proof of its correctness: https://github.com/seL4/l4v

The proof is much, much more work than the microkernel itself. A proof for something as large as webP might take decades.

When something like the seL4 microkernel is formally verified, the remaining bugs should only be bugs in the specification, not the implementation.

seL4 specifications and proofs are not a programming language.

Yes, especially 'logically impossible' when you dig into the details. From the blogpost:

> and the kernel modifications to seL4 that can reclaim the memory used by the rootserver.

MMMMMMMMMMMkkkkkk. So you then have to ask: were these changes also formally verified? There's a metric ton of kernel changes here: https://github.com/AmbiML/sparrow-kernel/commits/sparrow but I don't see a fork of https://github.com/seL4/l4v anywhere inside AmbiML.

I mean, it does also claim to be "almost entirely written in Rust", which is true if you ignore almost the entire OS part of the OS (the kernel and the minimal seL4 runtime).

I mean, just look at the commits with "fix" in the specs folder: https://github.com/seL4/l4v/commits/master?after=4f0bbd4fcbc...