[dwheeler]

Excellent, it's easy! Why haven't you completed this yet? :-)

So, a few thoughts.

The CSmith paper "Finding and Understanding Bugs in C Compilers" is a fun paper: https://www.cs.utah.edu/~chenyang/papers/pldi11-preprint.pdf - however, let's delve further. They found defects in every compiler they tried, proprietary and OSS. They even found defects in CompCert - because they were defects in CompCert’s unverified front-end code. What's more, they focused on "atypical combinations of C language features" - which are important, but to far fewer users.

Yes, it'd be awesome to have compilers that are perfect have absolutely no defects. Let's work on that. But it will be many, many years before they are widespread.

Besides, while no-defects would be awesome, many people are more interested in a different and simpler requirement - they want to detect subversion of binaries (where the binary and source do not correspond). Yes, provably perfect compilers could do that, but you don't need to wait for them; reproducible builds and DDC can provide that now, and you don't have to wait for anything.

So let's talk about VLISP. VLISP spawned an amazing number of papers, and was interesting work. Where's the code? MITRE never released it to my knowledge. To me, programs I can't run are in the "who cares?" category, and stuff people can't reproduce & investigate isn't really science anyway. Besides, VLISP only generated code for computers people generally don't use anymore. (You'll notice that I posted the scripts demonstrating DDC so that others can reproduce their execution.)

Sure, p-code was awesome in its time, I used it. But when newer hardware (the IBM PC) came along, it got superceded. More importantly for our story, it got superseded before there was time to develop any complex proofs. This is a more general problem: As long as formal proofs demand a massive amount of time, their results will become useless due to obsolescence. We must improve the tooling and models so that the proofs and layers can be done in a much faster and cost-effective way. Proving obsolete stuff is not very helpful. I think the ProVal approach (using Why3) is especially promising, but fundamentally, we need to make it not a massive research effort to write a high-assurance compiler.

Oh, and a little out-of-scope: As someone who's written Scheme & Common Lisp for decades, the problem with Lisp isn't its imperative nature; lots of people like Elm and Haskell, which are also functional languages. The problem with Lisps is their hideous syntax; Lisps don't even support infix by default, something every grade schooler learns. One solution is here: http://readable.sourceforge.net/

Anyway, what you've outlined is basically a program to build up from small safe components into larger trustworthy components. It's a sound strategy, and one that has been repeatedly advocated for decades by many people. But we also need to admit that it's going to take a long time, because our tooling is only just becoming good enough, and even then only in certain cases. There are serious limitations you're glossing over.

Don't ignore shorter-term smaller wins; they're valuable.

[srtjstjsj]

We all should have your ability to cheerfully and respectfully reply to disdainful sneers. Thank you.

[nickpsecurity]

I'm disagreeing with a person I respect on complicated topic rather than offering "disdainful sneers." I do respect how he replies to the disagreement. A scholar and a gentleman he is.

[nickpsecurity]

"Excellent, it's easy! Why haven't you completed this yet? :-)"

I did. Anyone that ever wrote their own Scheme, Oberon, or C compiler in primitive language did. Common assignment in classrooms. :P Anyway, I took a brain injury in an accident that cost me most of my memory back in 2011 or... idk. It's also hard to retain new things. People were amazed at what I've put together on hardware & some other stuff but I can't remember how to program hands-on, do set theory, a bunch of things. Only what I repeated a lot in year(s) leading up to injury. Unfortunately, I was in resaerch rather than build mode then. :(

Meanwhile, I still got enough fragments and learning ability to work on high-level passing stuff onto specialists. I've been mostly focused on solving secure hardware since most of rest is already done to point people can just build it from published techniques with some effort put in. Got digital, mask, and fab stuff pretty far but analog, RF, and EMSEC might be uncheatable. Might actually need years to decades of specialist knowledge for solution. (sighs) Also do lots of evangelism of high-assurance methods on various areas. However, the lack of effort on this very important problem in compiler assurance has led me to consider rolling up my sleeves and bumbling my brain-damaged ass through a compiler project with maybe this start:

http://schemeworkshop.org/2006/11-ghuloum.pdf

That, similar in PreScheme, or redo Oberon or Component Pascal. Then use those to build the rest. Who knows. Just a lot of stuff to relearn. QBE is nice on C side as it's simple plus has small number of high-bang-for-buck optimizations. So, if I did it, I'd recode that in CakeML with me checking initial tool (eg simple scheme/ML) by hand in assembly. I also found a way to do C code (or C compatible code) in ML. So there's options if I decide to take up your challenge. :)

"So let's talk about VLISP. "

I lost too many bookmarks in recent crash. I had a link to the page which had what looked like a downloadable Scheme48. The code generation was done for x86, PPC, ARM, and C language. You bet you can buy those today. Anyway, I'd do a current project in Myreen's LISP or CakeML if I wanted verification as they're current, maintained, and have more assurance. Actually, my scheme is side-by-side a fast version for development pace and safe verion for reference/production if not too slow. So, MLton and CakeML or (fast LISP here) and VLISP/LISP1.5. I theorize I'd get best of both worlds that way.

"We must improve the tooling and models so that the proofs and layers can be done in a much faster and cost-effective way."

Totally agree. I can't say which will win. Why is good. Lean is interesting. Coq & Isabelle/HOL are getting good libraries. Dependent types are faster but controversial. C has LiquidTypes, Frama-C, and Microsoft's VCC plus lots of static analysis. Don't know where it will go but doing anything critical in a functional language will definitely help. Certify equivalence to imperative for distribution. Just look at what productivity vs expertise COGENT achieves in the filesystem paper vs seL4 verification in Haskell/HOL/C:

https://ts.data61.csiro.au/projects/TS/cogent.pml

re LISP syntax.

I agree and thanks for Readable. Looks nice! Prior work I saw on this was Dylan language from Apple. Unfortunately didn't get adoption. Maybe time for another shot at beautiful, system LISP given Clojure's success.

" But we also need to admit that it's going to take a long time, because our tooling is only just becoming good enough, and even then only in certain cases. There are serious limitations you're glossing over."

I'm actually ignoring them on purpose to get a short-term win as you put it. Specifically, I'm expecting incremental, well-tested, inspectable compiler without expecting formal verification. I list it as necessary for full-trust but not necessary to get baseline up. The Goulum paper I linked and Scheme examples shows how little work first steps are if one uses published techniques & tooling good for job. Case in point by one person:

https://speakerdeck.com/nineties/creating-a-language-using-o...

The next component is keeping the implementation simple and putting in DbC-style interface checks in there. Initial quality comes from inspection, testing, modularity, and mostly pure interfacing. Overtime these two extra things allow high-assurance crowd to rewrite each pass using whatever tech they have available.

In case I'm not being clear, let me illustrate with example. The CompCert compiler verified compilation by using cleanly-defined passes into intermediate languages with specific steps on each. The medium-assurance approach just does that in Ocaml and/or CakeML with testing, QuickCheck, assertions, etc. Like regular development with slightly more effort and little expertise. The passes are also kept simple enough that their assurance can go up plug-and-play over time with others' help when they formally verify them. This can work with any software that doesn't channge a lot at once with usefulness over time. This includes compilers, protocols (esp SSL), key OS components, provers, standard libraries, maybe even parts of databases. I call it, similar to hardware field, Design for Verification for software. Like Orange Book B3, just spec, structure, and code it enough that it might get improved later.

Meanwhile, you get immediate benefits over a less-structured, monolithic compiler in C or C++ without things like QuickCheck or assertion-based, test generation. You also get more overtime without extra work if large uptake causes CompSci to focus on it. I cheat by recommending the ML stuff they already focus on. So, yeah, I'm all about interim stuff that doesn't need full, formal verification. If only because I both lack time and memory to use formal verification myself. Gotta help the new kids get finished faster and easier so I can trust/use the compiler, too! :)

[dwheeler]

> I did. Anyone that ever wrote their own Scheme, Oberon, or C compiler in primitive language did. Common assignment in classrooms. :P

Well... you implemented a compiler. And hey, that's a great thing. I've implemented several myself. But I doubt that you proved that it was correct, or that it was a large-enough language that many people would want to use it directly. :-).

> I'm actually ignoring them on purpose to get a short-term win as you put it. Specifically, I'm expecting incremental, well-tested, inspectable compiler without expecting formal verification. I list it as necessary for full-trust but not necessary to get baseline up.

Okay. But as you note, you're also focusing on shorter-term wins... they're just different shorter-term approaches for for different goals. And that's okay.

[nickpsecurity]

"Well... you implemented a compiler. And hey, that's a great thing. I've implemented several myself. But I doubt that you proved that it was correct, or that it was a large-enough language that many people would want to use it directly. :-)."

You got me there. Nobody wanted to pay me for it or anything haha.

"but as you note, you're also focusing on shorter-term wins... they're just different shorter-term approaches for for different goals. And that's okay."

Fair enough. I'm going to continue on my route for this topic, though, given there's already a lot of attention on the other ones. Parallel searches sometimes bear fruit. If it goes nowhere, you can bet I still have a copy of your papers and the reproducible build stuff so I can jump on that. :)