5 ms·
Coq: The World's Best Macro Assembler? (2013) [pdf]
- throwaway198846 11mo agoThey are going by Rocq today
- AdieuToLogic 11mo agoThe linked PDF was created on 8/5/13.
- volemo 11mo agoI understand and respect the renaming, Coq was a much cooler name though.
- graemep 11mo agoIt was. Renaming languages to suit American taste really grates. Nimrod to Nim was even worse. Apparently Americans cannot get Biblical references.
- UltraSane 11mo agoWhat if it was the word for Penis in Japanese or Chinese? I would understand them for changing it.
- gryn 11mo agothen we should change bit(s) because it means dick/penis in french /s
- School-Cotton 11mo agobit (in English) is not pronounced the same as bite (in French). The French word is closer in pronunciation to “beet” or “beat” in English. Also, “coq” and “cock” are not really pronounced the same either. The English word with the closest pronunciation to “coq” is “coke”.
- Narishma 11mo ago> bit (in English) is not pronounced the same as bite (in French). The French word is closer in pronunciation to “beet” or “beat” in English. Wrong, it's pronounced exactly like the English "bit".
- School-Cotton 11mo agoThat’s not true, at least in France. Perhaps it’s true in some other dialect, e.g. Quebec French; I don’t know. From Wiktionary, the pronunciation of English bit is /bɪt/, and French bite is /bit/. The sounds represented in IPA by ɪ and i are not the same, which is precisely why “bit” and “beet” sound different to Americans.
- Narishma 11mo agoI am from France. It's pronounced exactly the same here. Kids always joke about it when they first learn the English word 'bit'.
- School-Cotton 11mo agoI don’t doubt that you speak French. French people tend to have difficulty distinguishing those sounds because they are not distinguished in French. In English, they are: English has a much larger inventory of distinct vowel sounds than French (or indeed most European languages). In typical French-accented English, “bit” is indeed pronounced like the French word “bite”, but in native speaker English, it is not. I am a native speaker of American English and also speak French quite well. If you neither accept personal experience, nor what is written on Wiktionary, what evidence would you accept?
- dugmartin 11mo agoNot biblical references but rather Elmer Fudd. Bugs Bunny called Elmer Fudd "Nimrod" in a 1940's cartoon to sarcastically refer to Elmer as a great hunter. At that time I think most people probably got the biblical reference. Over time that word morphed into meaning something like an idiot to most Americans due to that cartoon. The same thing happened to the word "Acme" - the coyote in the road runner cartoons bought all his devices from the "Acme Corporation". Acme means the best/peak and it was a sarcastic reference to none of the gadgets ever working. Now most American's think Acme means generic/bad. They should have kept the name as Nimrod and named the package manager Acme instead of Nimble.
- addaon 11mo agoPoster here. I re-read this paper about once a year. I continue to think that it may be one of the most important papers I've read. As someone who works on high-reliability safety-critical real-time systems (automotive, avionics), being able to work in an environment where I could prove semantic properties of assembly code is pretty close to my dream -- the cost of demonstrating code correct is already so much higher than the cost of writing the code that the incremental cost of going to assembly seems minor, if there's even a small payback in time to demonstrate correctness. In practice, I think my dream language would be a relatively rich macro assembler plus a (guided, greedy) register allocator, designed entirely to simplify and allow semantic proofs. I don't really have a sense as to whether Coq (Rocq) is the right answer today, vs other options; or if there's a newer literature advancing this approach; but I'd truly love to see a deeper focus of making low level languages more useful in this space, rather than moving towards more constrained, higher level languages.
- kragen 11mo agoHave you found Coq or other formal-methods tooling useful?
- addaon 11mo agoNo, I haven't, but I want to. I haven't had the opportunity to go deep into formal methods for a work project yet, and on personal projects I've mostly played with Ada SPARK, not Coq. I've played with Coq a little (to the extent of re-implementing the linked paper for a subset of a different ISA), but there's definitely a learning curve. One of my personal benchmark projects is to implement a (fixed-maximum-size) MMM heap in a language, and convince myself it's both correct and of high performance; and I've yet to achieve that in any language, even SPARK, without leaning heavily on testing and hand-waving along with some amount of formal proof. I've written the code and comprehensive testing in various assembly languages (again, this is sort of my benchmark bring-up-a-new-platform-in-the-brain example), and I /think/ that for the way I think proving properties as invariants maintained across individual instructions maps pretty well to how I convince myself it's correct, but I haven't had the time, depth, or toolchain to really bottom any of this out.
- quanto 11mo agoThis paper reminds me of a class assignment in grad school where the prof asked the students to write a compiler in Coq for some toy Turning-complete language in a week. Having no background in compiler design or functional programming, I found it daunting at first, but eventually managed it. The Coq language's rigor really helps with something like this. I wonder if AI's compute graph would benefit from a language-level rigor as of Coq.
- kragen 11mo agoThe canonical URL, dating back to at least 02015, may be http://research.microsoft.com/en-us/um/people/nick/coqasm.pdf http://research.microsoft.com/en-us/um/people/nick/coqasm.pd..., which now redirects to https://www.microsoft.com/en-us/research/publication/coq-worlds-best-macro-assembler/ https://www.microsoft.com/en-us/research/publication/coq-wor.... This site presumably belongs to the Nick Benton who is one of its authors.
- asdefghyk 11mo agoThe x86 architecture and instruction set is complex - so it absolutely needs a powerful assembler to help prevent mistakes.
- kragen 11mo agoThat doesn't seem right to me. If the problem is that it has too many instructions and addressing modes, you can decide to only use a small subset of those instructions and addressing modes, which really isn't much of a handicap for implementing functionality. (It doesn't help with analyzing existing code, but neither does a powerful assembler.) I'm no expert on assembly-language programming, but probably 90% of the assembly I write on i386, amd64, RISC-V, and ARM is about 40 instructions: ldr, mov, bl, cmp, movs, push, pop, add, b/jmp, bl/blx/call, ret, str, beq/jz, bne/jnz, bhi/ja, bge/jge, cbz, stmia, ldmia, ldmdb, add/adds, addi, sub/subs, bx, xor/eor, and, or/orr, lsls/shl, lsrs/sar/shr, test/tst, inc, dec, lea, and slt, I think. Every once in a while you need a mul or a div or something. But the other 99% of the instruction set is either for optimized vectorized inner loops or for writing operating system kernels. I think that the reason that i386 assembly (or amd64 assembly) is error-prone is something else, something it has in common with very simple architectures and instruction sets like that of the PDP-8.
- yjftsjthsd-h 11mo ago> I think that the reason that i386 assembly (or amd64 assembly) is error-prone is something else, something it has in common with very simple architectures and instruction sets like that of the PDP-8. What reason is that? (And, if it's not obvious, what are ARM/RISC-V doing that make them less bad?)
- kragen 11mo agoI don't think they're particularly less bad. All five architectures just treat memory as a single untyped array of integers, and registers as integer global variables. Their only control structure is goto (and conditional goto.) If you forget to pass an argument to a subroutine, or pass a pointer to an integer instead of the integer, or forget to save a callee-saved register you're using, or do a signed comparison on an unsigned integer, or deallocate memory and then keep using it, or omit or jump past the initialization of a local variable, conventional assemblers provide you no help at all in finding the bug. You'll have to figure it out by watching the program give you wrong answers, maybe single-stepping through it in a debugger. There are various minor details of one architecture or the other that make them more or less bug-prone, but those are minor compared to what they have in common. None of this is because the instruction sets are complex. It would be closer to the mark to say that it's because they are simple.
- mmastrac 11mo agoIt's a bit of an awkward syntax to get a reliable assembler. Does it at least allow you to prove the behaviour of a larger block of assembly? For example, could I use it to prove that a block of assembly is equivalent to a given set of operations?
- kragen 11mo agoYes.
- anthk 11mo agoA Lisp can mimic Prolog and the rigour of Coq with ease.
- attila-lendvai 11mo agoi'm a long time lisper, but i don't think this is justified. implementing prolog/backtracking on top of lisp is certainly possible and not even too hard (see e.g. https://github.com/nikodemus/screamer https://github.com/nikodemus/screamer) and implementing Coq on top of lisp is also possible. but IMO the "with ease" phrase is not justified in this context. if you only mean that lisp will not be in the way if you set out to implement these, then i agree. lisp -- the language and the typical opensource implementation -- will be much less of an obstacle than other languages when chosen as foundations.
- addaon 11mo agoCan you give an example? With something like Figure 1 of the paper converted to a convenient form for Lisp (s-expressions, presumedly), and assuming a function to convert it to binary, what would it look like to prove correctness of that assembly in Lisp? What's the ecosystem of proof assistants that would get you there?
- kragen 11mo agoYou can write a prover like Coq in a Lisp, but, though it's easier than doing it in C, I think it's somewhat harder than doing it in something like OCaml. ACL2 is an example of such a thing.
- dang 11mo agoDiscussed at the time: Coq: The world’s best macro assembler? (2013) [pdf] - https://news.ycombinator.com/item?id=8752385 https://news.ycombinator.com/item?id=8752385 - Dec 2014 (61 comments)
- Svoka 11mo agoThis is great. I honestly never thought of computer as a register state and instructions/asm commands as functions applied to it. But that makes so much sense.
- peter_d_sherman 11mo ago>"3. Assembling x86 A particular emphasis of our work on machine code verification is on using Coq as a place to do everything: modelling the machine, writing programs, assembling or compiling programs, and proving properties of programs. Coq’s powerful notation feature makes it possible to write assembly programs, and higher-level language programs, inside Coq itself with no need for external tools." Looks very promising! There is definitely something here!