'Proof Theory Impressionism: Blurring the Curry-Howard Line' by Dan Pittman

The Curry-Howard Correspondence is the observation that there exists a correspondence between objects present in disparate formal systems. Once such instance of this correspondence is the conspicuous propositions-as-types notion, which draws correspondences between logical propositions and types in a programming language.

As another more specific instance, one could consider a program written in a traditional programming language like Rust, and its formal proof exercised in a language like Coq.

While this is a beautiful revelation in theory, in practice this line begins to look more like an impenetrable wall as it divides proof from program. This chasm prevents assurances that, beyond those that can simply be "observed" by a human, an implementation faithfully abides its proofs. The conventional solution to this problem is code extraction. However, in cases like safety-critical system software (e.g. avionics, medical devices, & autonomous vehicles), the languages and platforms targeted by extraction tools simply aren't an option. What if there was another way?

This talk explores some potential approaches to endow our production language, mostly Rust in this case (w/ a dash of Haskell), with the capabilities present in "provable" systems. These explorations will include spaces like totality, type-level programming, and dependent types. Ultimately drawing lines from the above explorations back to how one might write such a thing in the language of a proof assistant.

Speaker: Dan Pittman

[TAiCkIne-TOrESIve]

6:21 Lean4 extracts C programs although the extraction process doesn't seem to have been formally verified. There is also ATS-lang that builds proofs around existing C code.

[BethKjos]

It would be fabulous to see an update after oh these many moons: How much success did the project see? Where is it used? Have the standards bodies figured out about toolchain integrity?

[ilyabobyr]

It would be nice to hear the questions =)

[a.s.]

25:20 25:54
if bugs come at big price (loss) - language with more (longer) typing (enforced correctness) needed.
if bugs are costless (or acceptable) - language with less typing will do the job much quicker.

[tricky]

If a program loads an ECU such that the ECU draws too much current, the PSU voltage drops and a driver alert doesn't sound then would this fall under the problem of operational semantics in the same way as the example that deletes the filesystem? If so then, given people never seem to give load and memory activity/occupancy any consideration with denotational semantics, how are denotational and operational semantics different? Is it just a question of awareness? IE, if you are aware there are files and they can be absent then to consider them is denotational semantics and to ignore them wilfully is operational semantics - but if you're not aware then it's all denotational semantics?

[NikolajLepka]

Dependent types are the complex numbers of type theory.
They fill a gap previously present, and is archaic enough that the layman will probably never interact with it

[hankigoe]

5:00 The proof worked b/c 'lol' happens to be a palindrome. It would have failed on 'haha' :D

[dengan]

Didn't they already solved this problem with sel4 kernel?
It has been fully proved, but written in C, not rust. Then auto translated into Isabelle /HOL.