Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Coq: The World's Best Macro Assembler? (2013) [pdf]

nickbenton.name

Post reply on HN
Print view View original

21–30 of 75 posts

Re: Coq: The World's Best Macro Assembler? (2013) [pdf]

#21

Post by tensegrist »

quanto wrote: post #12
addaon wrote: post #4

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…

During the days I was studying/working with Coq, one visiting professor gave a presentation on defense software design. An example presented was control logic for F-16, which the professor presumably worked on. A student asked how do you prove "correctness", i.e. operability, of a jet fighter and its control logic? I don't think the professor had a satisfying answer. My question is the same, albeit more technically r…

> There are documented tragedies where numerical rounding error of the control logic of a missile costed lives.

curious about this

Re: Coq: The World's Best Macro Assembler? (2013) [pdf]

#22

Post by gjadi »

addaon wrote: post #14
kragen wrote: post #10

Earlier quoted context omitted.

Have you found Coq or other formal-methods tooling useful?

No, 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…

What's a MMM heap? Is it a typo on min-max heap?

Re: Coq: The World's Best Macro Assembler? (2013) [pdf]

#24

Post by codenaught »

tensegrist wrote: post #21
quanto wrote: post #12

Earlier quoted context omitted.

During the days I was studying/working with Coq, one visiting professor gave a presentation on defense software design. An example presented was control logic for F-16, which the professor presumably worked on. A student asked how do you prove "correctness", i.e. operability, of a jet fighter and its control logic? I don't think the professor had a satisfying answer. My question is the same, albeit more technically r…

> There are documented tragedies where numerical rounding error of the control logic of a missile costed lives. curious about this

This is likely a reference to the Patriot missile rounding issue that arguably led to 28 deaths.

https://www-users.cse.umn.edu/~arnold/disasters/Patriot-dhar...

https://www.gao.gov/assets/imtec-92-26.pdf

Re: Coq: The World's Best Macro Assembler? (2013) [pdf]

#25

Post by throw-qqqqq »

kragen wrote: post #10
addaon wrote: post #4

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?

I have found huge value in CBMC and KLEE for statically verifying C code for real time safety critical embedded applications.

ACL2 is also VERY powerful and capable.

Re: Coq: The World's Best Macro Assembler? (2013) [pdf]

#27

Post by anthk »

dwohnitmok wrote: post #15
quanto wrote: post #12

Earlier quoted context omitted.

During the days I was studying/working with Coq, one visiting professor gave a presentation on defense software design. An example presented was control logic for F-16, which the professor presumably worked on. A student asked how do you prove "correctness", i.e. operability, of a jet fighter and its control logic? I don't think the professor had a satisfying answer. My question is the same, albeit more technically r…

You use floating point numbers instead of real numbers in your theorems and function definitions. This sounds flippant, but I'm being entirely earnest. It's a significantly larger pain because floating point numbers have some messy behavior, but the essential steps remain the same. I've proved theorems about floating point numbers, not reals. Although, again, it's a huge pain, and when I can get away with it I'd pref…

You use reducing rationals everywhere you can, not floast.

Re: Coq: The World's Best Macro Assembler? (2013) [pdf]

#28

Post by sylware »

addaon wrote: post #4

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…

The second your macro-assembler has a significantly complex syntax, you are done: feature creep for 2042 features then 2043 then 2044... and it mechanically reduces the number the alternative implementations and make the effort required to develop a new more and more unreasonable.

In this end, it is all about the complexity and stability in time for this matter.

Re: Coq: The World's Best Macro Assembler? (2013) [pdf]

#29

Post by oersted »

codenaught wrote: post #24
tensegrist wrote: post #21

Earlier quoted context omitted.

> There are documented tragedies where numerical rounding error of the control logic of a missile costed lives. curious about this

This is likely a reference to the Patriot missile rounding issue that arguably led to 28 deaths. https://www-users.cse.umn.edu/~arnold/disasters/Patriot-dhar... https://www.gao.gov/assets/imtec-92-26.pdf

Just to clarify for others because it’s a tiny bit clickbaity:

The Patriot missile didn’t kill 28 people accidentally, it simply failed to intercept an enemy missile.

And it wasn’t launched on an incorrect trajectory either, the radar was looking at a slightly wrong distance window and lost track. Furthermore, the error only starts having an effect after 100 hours of operation, and it seems to have only been problematic with the faster missiles in Iraq that the system wasn’t designed for. They rushed the update and they did actually write a function to deal with this exact numerical issue, but during the refactor they missed one place where it should have been used.

28 lives are obviously significant, but just to note that there are many mitigating factors.

Re: Coq: The World's Best Macro Assembler? (2013) [pdf]

#30

Post by graemep »

volemo wrote: post #5
throwaway198846 wrote: post #2

They are going by Rocq today

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.

Post reply on HN