vale

There's Vale [0] as a structured high-level assembly language, but pretty far from usable right now. I do hope it matures. Basically: All non-control-flow instructions can be directly supported. Control flow is lofted to a higher level and implemented in C-style structured blocks and keywords, which map directly to a subset of the ISA that modifies the program counter. This separation means it's not a proper superset of traditional assembly languages -- you can't paste in arbitrary blocks of existing code -- but a lot of interesting things (for them, implementations of cryptographic primitives) are pretty trivial to port over. And in exchange, you get a well defined Hoare logic that can talk about total correctness, not just [1]'s partial correctness. [0] https://github.com/project-everest/vale [1] https://nickbenton.name/coqasm.pdf

This actually has already been done in OS research. https://en.m.wikipedia.org/wiki/Verve_(operating_system) https://en.m.wikipedia.org/wiki/Typed_assembly_language Which eventually grew to stuff like this, https://github.com/project-everest/vale

Given the possible confusion with Vale[1] and Vala[2], I suggest to rename the language to some new unambiguous name asap in order get more visibility. Otherwise, it looks very promising! [1] https://github.com/project-everest/vale [2] https://en.m.wikipedia.org/wiki/Vala_(programming_language)

This. Big part of the most high-performance code (like crypto, linear-algebra or fft kernels) are even generated: you build a program that will generate a program that will get compiled (or is already asm). One can arguably say that the generator program is part of the compiler chain (takes parameters describing some algorithm and generates executable code). And these generators sometimes call out to SMT solvers or otherwise solve complicated algorithmic problems (integer programming problems for vectorizing with the polyhedral model). Hence these are specialized high-level compilers that take a long time to output extremly fast and small programs. Most people don't call the generators tho, they only use the generated code: long compilation time is no problem if you have good modular compilation. http://www.fftw.org/ http://flopoco.gforge

You could write those in Vale[0], but at that point, just use miTLS[1] to have a completely verified TLS implementation. [0] https://github.com/project-everest/vale [1] https://mitls.org/

Before I submitted it to Lobsters, I checked the "Source Code" part of the link, allowed a few scripts in NoScript, and got this page with .v files that at least looked like the source code: https://x86proved.codeplex.com/SourceControl/latest#src/ I'm a guy that tracks and reports on progress in this specialty but not a trained specialist. I don't know Coq well enough to tell you if this is the source code to the CoqASM paper with the quick skim I did before work. I do know it has a bunch of .v files going into detail about x86 and some other things with some overlap in aspects I thought I read about in the older paper. Hence, the submission claiming it was probably the same thing. While we're at it, here's some other links on this sort of thing all of you might enjoy: http://www.cs.cornell.edu/talc/ https://project-everest.github.io/asse

One step is making sure that the crypto isn't bogus. That's what this formal verification is about here. The next step would be writing an implementation in a language that's verifiable -- such as F* [1] -- and then using that to output actually verified binaries. People are indeed working on this kind of thing, to the point where even the primitives are being generated in this way, such as the HACL* and Vale projects [2] [3]. These are in service of making a verified TLS stack. It's nicely modularized and some of this might, at some point in time, be used for a verified WireGuard implementation. Or, alternatively, other unrelated methods for that. These are exciting times in the formal methods space. In any case, this paper is about the first -- and incredibly important -- step of that kind of journey: making sure the crypto construction