41–50 of 75 posts
A Lisp can mimic Prolog and the rigour of Coq with ease.
Earlier quoted context omitted.
I understand and respect the renaming, Coq was a much cooler name though.
It was. Renaming languages to suit American taste really grates. Nimrod to Nim was even worse. Apparently Americans cannot get Biblical references.
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.
Earlier quoted context omitted.
I 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…
I have a postit note idea that says simply "typesafe macro assembler". I've not fleshed this out yet, but I think a relatively simple system would help deal with all the issues you mention in the first paragraph while allowing escape hatches.
Poster 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…
Have you found Coq or other formal-methods tooling useful?
Amazon AWS uses Dafny to prove the correctness of some complex components.
Then, they extract verified Java code. There are other target languages.
Being based on Hoare logic, Dafny is really simple. The barrier of entry is low.
Earlier quoted context omitted.
What if it was the word for Penis in Japanese or Chinese? I would understand them for changing it.
then we should change bit(s) because it means dick/penis in french /s
Also, “coq” and “cock” are not really pronounced the same either. The English word with the closest pronunciation to “coq” is “coke”.
It'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?
A Lisp can mimic Prolog and the rigour of Coq with ease.
Earlier quoted context omitted.
Have you found Coq or other formal-methods tooling useful?
I have found Isabelle very useful, and Dafny even more so. Amazon AWS uses Dafny to prove the correctness of some complex components. Then, they extract verified Java code. There are other target languages. Being based on Hoare logic, Dafny is really simple. The barrier of entry is low.
Earlier quoted context omitted.
> when I can get away with it I'd prefer to prove things with real numbers and assume magically they transfer to floating point. True for some approaches, but numerical analysis does account for machine epsilon and truncation errors. I am aware that Inria works with Coq as your link shows. However, the link itself does not answer my question. As a concrete example, how would you prove an implementation of a Kalman fi…
I'm curious about how you'd do that, too. I haven't tried doing anything like that, but I'd think you'd start by trying to formalize the usual optimality proof for the Kalman filter, transfer it to actual program logic on the assumption that the program manipulates real numbers, try to get the proof to work on floating-point numbers, and finally extract the program from the proof to run it. https://youtu.be/_LjN3UclY…
Earlier quoted context omitted.
then we should change bit(s) because it means dick/penis in french /s
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. Also, “coq” and “cock” are not really pronounced the same either. The English word with the closest pronunciation to “coq” is “coke”.
Wrong, it's pronounced exactly like the English "bit".