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

61–70 of 75 posts

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

#61

Post by Narishma »

School-Cotton wrote: post #56
Narishma wrote: post #50

Earlier quoted context omitted.

> 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".

That’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.

I am from France. It's pronounced exactly the same here. Kids always joke about it when they first learn the English word 'bit'.

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

#62

Post by kragen »

addaon wrote: post #39
throw-qqqqq wrote: post #25

Earlier quoted context omitted.

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.

I'd love some examples here.

So would I!

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

#63

Post by dwohnitmok »

dwohnitmok wrote: post #54
quanto wrote: post #16

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…

The link was to show Coq's floating point library. > As a concrete example, how would you prove an implementation of a Kalman filter is correct? This would be fun enough to implement if I had more time. But I need to spend time with my family. I'm usually loathe to just post LLM output, but in this case, since you're looking just for the gist, and I don't have the time to write it out in detail, here's some LLM outpu…

Error in `f1_equal_to_f2`. Should be ` f1_equal_to_f2 : forall (x: Float), floatToR(f1(x)) = f2(floatToR(x))` with an implicit proof delivered to `f2` that `forall (x: R), IsFloat(floatToR(x))`.

Also there's some subtleties in how to set up the code extraction to make sure you don't inadvertently extract other real-valued functions, but this is already too long.

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

#64

Post by School-Cotton »

Narishma wrote: post #61
School-Cotton wrote: post #56

Earlier quoted context omitted.

That’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.

I am from France. It's pronounced exactly the same here. Kids always joke about it when they first learn the English word 'bit'.

I 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?

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

#65

Post by UltraSane »

Narishma wrote: post #50
School-Cotton wrote: post #45

Earlier quoted context omitted.

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”.

> 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".

https://forvo.com/word/une_bite/

This French guy says it exactly like the English word beet.

https://www.merriam-webster.com/dictionary/bit

English bit.

https://www.merriam-webster.com/dictionary/beet

English beet

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

#66

Post by nothrabannosir »

Narishma wrote: post #61
School-Cotton wrote: post #56

Earlier quoted context omitted.

That’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.

I am from France. It's pronounced exactly the same here. Kids always joke about it when they first learn the English word 'bit'.

It's pronounced the same only by people speaking English with a French accent. An American, Brit, Indian, or any other native speaker of English absolutely does not pronounce "bit" the same way a French person pronounces "une bite."

Rather than measuring whose French pedigree is longer, I will put down a wager on this. ₹3? :D

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

#67

Post by ajb »

kragen wrote: post #51
thesmtsolver wrote: post #49

Earlier quoted context omitted.

It is really not that difficult. Here is a paper that formalizes a version of feed forward networks to prove properties about them. https://arxiv.org/pdf/2304.10558

I only skimmed this paper, but it doesn't mention floating point (it's only modeling the FNN as a function on reals), and I don't think you can extract a working FNN implementation from an SMT-LIB or Z3 problem statement, so I think you have to take on faith the correspondence between the implementation you're running and the thing you proved correct. But that's the actual problem we're trying to solve; nobody really…

In most cases the data a kalman filter is working on has some precision which is much lower than the available precision in the floating format you are using. The problem is inherently a statistical one, since the expected precision depends on the statistics of your data source.

So you would probably adopt some conservative approach in which you showed that the worst case floating point rounding error is But, I think specialised tools are more commonly used than general process. Eg, see https://github.com/arpra-project/arpra

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

#68

Post by kragen »

ajb wrote: post #67
kragen wrote: post #51

Earlier quoted context omitted.

I only skimmed this paper, but it doesn't mention floating point (it's only modeling the FNN as a function on reals), and I don't think you can extract a working FNN implementation from an SMT-LIB or Z3 problem statement, so I think you have to take on faith the correspondence between the implementation you're running and the thing you proved correct. But that's the actual problem we're trying to solve; nobody really…

In most cases the data a kalman filter is working on has some precision which is much lower than the available precision in the floating format you are using. The problem is inherently a statistical one, since the expected precision depends on the statistics of your data source. So you would probably adopt some conservative approach in which you showed that the worst case floating point rounding error is But, I think…

That's a start, but you might be able to do better than that; for example, you ought to be able to show that the floating-point rounding error is unbiased.

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

#69

Post by peter_d_sherman »

>"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!

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

#70

Post by dwohnitmok »

anthk wrote: post #27
dwohnitmok wrote: post #15

Earlier quoted context omitted.

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.

This is potentially horrendous for performance, and even worse, unpredictably so. Instead of getting the incorrect answer (or NaN) with floating point if you have an unfortunate series of calculations, you get extreme memory blowup, where your numerator and denominator can explode in size, which in turn leads to runtime slowdown. In the worst case you can actually run out of memory (because certain fairly natural calculations can cause your numerators and denominators to very rapidly explode in size).

Committing to unbounded rationals basically opens your system up to DoS attacks.

You could decide to bound rationals in the numerator and denominator, but then you've more or less reinvented a form of floating point.

In order of preference for a high reliability production system I would use:

1. Integers

2. Fixed point

3. Floating point

4. Rationals [waaaayyyy down in fourth place]

Most systems don't have high enough reliability needs though that I would favor fixed point over floating point and so in practice I rarely use fixed point (simply because library and language support is far worse).

Post reply on HN