#Pancake: a new, verified Pascal-like #pl emphasizing formal verification over type safety for low-level systems programming, device drivers in particular.
"Pancake eschews complex type systems to make the language attractive to systems programmers, while at the same time aiming to ease the formal verification of code. We describe the design of the language and its verified compiler, and examine its usability, performance and current limitations through case studies of device drivers and related systems components for an #seL4-based #os."
One of the challenges with the deployment of more automated reasoning is often the tooling. Cool to see #Cryspen invest in a new integrated development and verification environment based on hax. Congrats @franziskus and team :) https://cryspen.com/post/cyber-campus-hax/
⎧ The point is not so much that proofs are easier with Liquid Haskell, but rather that we are in front of an approach that integrates well with a programming language as is, and yet it leverages the power of tools specialized to reason about logic when verifying programs ⎭
Prompted by the recent thread/inquiry by @Patricia with @HalvarFlake’s reply I went to see if somebody was now working on applying formal methods to the eBPF verifier. Turns out there are some folks at the University of Texas at Austin that released a paper titled “Formal Verification of the Linux Kernel eBPF Verifier Range Analysis”
Hi everyone, I've been on Mastodon for a while but I'm new to hci.social - glad to finally find a federate that aligns with my interests. I have a background in #humanfactors, and I'm interested in human-machine teaming, human-automation interaction, and the application of #formalmethods and other rigorous mathematical approaches to these domains. Open to further discussion!