L1c: A conceptually simple formally verified compiler | Hacker News Reader

L1c: A conceptually simple formally verified compiler

github.com

33 pointsCHY8723 comments

I was going to suggest looking at FLINT certifying compiler and VeriML but with CakeML on your page you probably already know about these. I still have a suggestion to think on that I've only seen a bit of: macro-assembler for verification. Have a concept for it. Like Hyde's High Level Assembler, you create constructs (eg control flow or array operators) useful for implementing programs or say a compiler. You verify their implementation in such a way where people can just call a function and your code converts it directly into equivalent machine code. These can be composed into other routines where provers or analysis tools can more easily argue about the resulting properties. There's also a reuse aspect.

On other end, one uses an ML-like language, SPARK Ada, or something designed for easy verification to specify and test the behavior of the software. Like FLINT or Cleanroom, one breaks it down into functions amendable to analysis or verification. Those functions' implementations are done in a way that can straight-forward albeit tediously written in the verified, macro-asm. Human review and test-centered equivalence checking argues correspondence at first with formal methods later if desired. Run verified asm toolchain on it to get a correctness argument that your app's source equals machine code. If your app is a compiler, you will have many more without hand-doing the macro-asm and a bunch of verified macro's to use in next app. ;)

What do you think about macro-asm + formal methods for verified component construction ground up + top down? Any potential you see?

Note: My scheme was inspired by both VLISP and Wirth's Lilith machine. VLISP implemented PreScheme first then used it to implement the full software. Wirth implemented a more ideal processor ISA, M-code, that represented things like stack operations with perfect Modula-2 compatibility. He then did a Modula-2 to M-Code compiler with the rest of the software written in Modula-2 w/ M-code for acceleration. For both systems, raising the machine level up a notch reduced their overall work and made the source more consistent throughout.

Looking at the proof: has the proof been formally verified? There could be a bug in that...

The proof is written in the HOL4 proof assistant. The idea here is the same as any LCF derivative- there is a type, thm, and the constructors of that type are constructed such that only valid theorems can be created. So, by creating a value of type thm, with that corresponding to your goal, you've proven the theorem.

My proof works by creating such a value.

There are obviously lots of places where this can go wrong, but good progress has been made towards most of them - http://materials.dagstuhl.de/files/15/15182/15182.KonradSlin... is a decent explanation.

As a handwavey argument, the proof could be incorrect, but if it were incorrect, the incorrectness would be more interesting than the current proof (i.e. a serious bug would have been located in the theorem prover).

Reply on news.ycombinator.com