i feel that the grammar of a programming language is among the least appropriate of all possible facets of its behavior to start off with.

[hipsterelectron@circumstances.run]

This difficulty, a direct consequence of the use of indirection,

how are you still negging the reader like this

can be broken down as the aliasing [14] and frame [61] problems.

oh my GOD!!!!! ok so these fucking citations my god

[14] this is literally about virtual memory conforming to the C standard https://eis.mdx.ac.uk/staffpages/r_bornat/papers/MPC2000.pdf

The final difficulty is the complexity of the proofs: not only do we have to reason formally about sets, sequences, graphs and trees, we
have to make sure that the locality of assignment operations is reflected in the treatment of assertions about the heap.

EVEN THAT PAPER'S AUTHOR IS TELLING HIM TO DO HIS FUCKING JOB LOL

For all of these reasons, Hoare logic isn’t widely used to verify pointer programs. Yet most low-level and all object-oriented programs use heap pointers freely. If we wish to prove properties of the kind of programs that actually get written and used, we shall have to deal with pointer programs on a regular basis.

[hipsterelectron@circumstances.run]

literally nothing will prepare you for [61]

[hipsterelectron@circumstances.run]

[61] McCarthy and P. Hayes. Some philosophical problems from the
standpoint of artificial intelligence. In D. Michie and B. Meltzer, editors,
Machine Intelligence 4, pages 463–502. Edinburgh University Press,
1969.

[dalias@hachyderm.io]

@hipsterelectron Ring 0 uses the MMU. Kernel setting up MMU to map physical memory directly is an implementation choice, not something inherent to being a kernel/ring0.

A good kernel wouldn't do that.

[hipsterelectron@circumstances.run]

only possible alternative is he mistyped the reference address making a crucial point in his own phd thesis

[62] F. Mehta and T. Nipkow. Proving pointer programs in higher-order
logic. Information and Computation, 199(1-2):200–227, 2005.

and yes, it still assumes the heap. even though if you're managing physical memory. you do not have a heap

[hipsterelectron@circumstances.run]

god fuck and even this example is literally impossible

For an example of aliasing, consider a program with two pointer variables int * p and int * q and the following triple:

{| True |} ∗p = 37 ; ∗q = 42 ; {| ∗p = ? |}

not only has he just said "triple" without a citation like that's a well-known thing, this is the problem with it:

We are unable to ascertain the value pointed to by p as it may refer to the same location as q.

so you're telling me this C code:

int * p;
int * q;
*p = 37;
*q = 42;

demonstrates a classic aliasing problem....................does this guy even know about restrict or the concept of Undefined Behavior

[hipsterelectron@circumstances.run]

turns out a "hoare triple" is the fuckboy term for "precondition and postcondition" when you think you're the first to ever create an abstract machine for the C programming language

he never cites anything about a Hoare triple either

Hoare triples, where a block of code is preceded by a pre-condition and followed by a post-condition, have already appeared in §1.1.1.

he did just refer you, with a hyperlinked section heading, to the line above where he just says "triple"

[hipsterelectron@circumstances.run]

The aliasing problem is much worse for inductively-defined data structures, where it is possible that structural invariants can be violated, and where we need more sophisticated recursive predicates to stipulate aliasing conditions.

this problem is so bad he has no example

These predicates appear in specifications, invariants and proofs, and their discovery is often a time consuming trial-and-error process.

sorry that you hate your job?

The aliasing situation becomes untenable when code is type-unsafe and we are forced to seek improved methods.

if the C compiler can unambiguously interpret it then maybe the C compiler is a better proof framework than isabelle/HOL

If instead we had a variable float * p:

{| True |} ∗p = 3 .14 ; ∗q = 42 ; {| ∗p = ? |}

then not only do we have to consider aliasing between pointers of different types, but also the potential for p to be pointing inside the encoding of ∗q and vice versa.

i don't know what language you're verifying but C has semantics here

We talk about this phenomenon as inter-type aliasing.

who's we

[hipsterelectron@circumstances.run]

While specifications may mention some state that is affected by the intended behaviour of a program, it is hard to capture the state that is not changed.

literally a nonsense sentence

In the above example, a client verification that also dereferences a pointer r, not mentioned in the specification, has no information on its value after execution of the code fragment.

meaningless

This limits reusability and hence scalability of verifications.

the C compiler is a better proof framework than isabelle/HOL

[hipsterelectron@circumstances.run]

now he's explaining why he trusts machine output more than anyone

Formal reasoning with the usual process of pen-and-paper mathematical proof neither scales as we would like in software verification nor has the expected degree of rigour.

you know humans made isabelle/HOL too right

[hipsterelectron@circumstances.run]

"scales" i think he literally just means deskilling here. he's literally saying actually formal verification is more reliable than engineers you pay money to

[hipsterelectron@circumstances.run]

now he's trying to mansplain "algorithmic verification" as if model checking in TLA+ https://lamport.azurewebsites.net/tla/high-level-view.html isn't actually extremely widely used in this exact space already

Research in this area has produced impressive results in recent years with improvements in the underlying theory and increased available computing power.

theory and computing power are the only things that produce impressive results. no i can't give you a citation it's not like this is my dissertation

They can catch increasingly wider classes of programmer errors

this is still a fucking hateful way to talk about formal verification

and even guarantee the absence of certain types of bugs.

such a half-assed phd thesis. do you even believe in what you're saying

[willow@social.translunar.academy]

@hipsterelectron TLA mentioned let's go

[freya@social.highenergymagic.net]

@Willow @hipsterelectron omg

[hipsterelectron@circumstances.run]

Proof creation has a high cost associated with it.

yeah you keep saying it sucks. aren't you supposed to fix things like that

To give an idea, it has been the author’s experience [93, 94, 96] that, in an interactive theorem prover, verifying the functional correctness of C code can require between one and two orders of magnitude more proof steps than line count,

(a) yeah maybe cause you keep trying to verify functional correctness guarantees about heap allocations in ring 0
(b) "line count" appeals to the VC class. it doesn't work on programmers

[hipsterelectron@circumstances.run]

literally everyone go read aaron turon's paper on weak atomic memory orderings right now https://plv.mpi-sws.org/gps/paper.pdf yes there's a coq proof but that's not what a paper is for!!!

check out this future work section:

However, the C11 model allows programmers to freely mix memory orderings, and ideally program logics should support such mixed reasoning as well.

literally it's that easy to give a shit about making people safe and providing powerful robust guarantees. this is why rust used to be good

Early investigation suggests that the C11 model has some corner cases when mixing memory orderings that may obstruct compositional reasoning principles.

i get nerd sniped every time i read that line lmao

[hipsterelectron@circumstances.run]

We believe the extra generality of GPS is important because it enables us to verify a wider class of weak memory programs, including those whose observable behavior is not SC. The circular buffer and Michael-Scott queue are good examples of this (see the appendix [1]). Singh et al. [35] argue that one should not expose the high-level programmer to such non-SC data structures, but GPS shows that in fact it is possible to reason sensibly and modularly about them.

keep in mind seL4 doesn't even represent concurrent behavior at all in their 2009 proof (as far as i can tell), even though concurrency semantics are a feature on any system with a motherboard. and aaron turon shows actually we can make it easier to write complex code with formal verification

[hipsterelectron@circumstances.run]

honestly i should totally mess around with coq semantics for my ring buffer from hell

[hipsterelectron@circumstances.run]

oh yeah the other guy was telling me how much it sucks to verify stuff

and in a single person year, we may be limited to verifying no more than something in the order of 1000 lines-of-code (LoC). Little data exists for how proof-based projects scale, but it is unlikely to be linear.

still just ridiculous that this guy is still talking "verification" without doing the work in the c compiler. i know people do that

The economics of verification have two significant consequences.

so bleak to talk about your research focus like this

First, the range of systems we can hope to verify is limited, but is still large enough to be practically interesting.

that's literally not a "consequence" why would you invoke proof jargon incorrectly lmao

Modern microkernels, with implementations around 10,000 LoC are hopefully within the realm of possibility.

you were just a moment ago saying int * p; int * q; was beyond your abilities

[astraleureka@social.treehouse.systems]

@hipsterelectron "ring buffer from hell" sounds incredibly exciting