fuklief

8 ms·

31.
by fuklief 7y ago
Credit card = Débit différé in France (aka. you pay for everything at the end of the month), it's even written Credit on the card. And most online banks (e.g., Boursorama, Hello Bank, Fortuneo, etc) do not charge you a monthly fee for
32.
by fuklief 7y ago
+1 What does it even mean that the language is formally provable ?!
33.
by fuklief 7y ago
CertiKOS is verified in Coq, I don't see why you say it isn't fit to get work done.
34.
by fuklief 7y ago
Currently, yes. Eventually, no.
35.
by fuklief 7y ago
Meanwhile, Google researchers (Plotkin and Abadi) are going to present "A Simple Differentiable Programming Language" at POPL20[1] in January. I can't find a preprint though :'( [1]: https://popl20.sigplan.org
36.
by fuklief 7y ago
I'm guessing at least the sponsors of the OCaml software foundation: https://ocaml-sf.org/sponsors/
37.
by fuklief 7y ago
Does it have to be tech related ? What if I want to make a small group to meet people for boardgames or something ?
38.
by fuklief 7y ago
CompCert ?
39.
by fuklief 7y ago
In my field, we use this kind of example to tell people that testing sucks or is not enough and that we need to formally/mathematically prove that software is free of bugs for critical systems.
40.
by fuklief 7y ago
The abstract says cryptoverif is a proof assistant, but the cryptoverif page says it's an automatic protocol prover. Which is it ? (my understanding is that a proof assistant is interactive, like Coq, Agda, etc)
41.
by fuklief 8y ago
> The mathematical proof might be 100% solid and hacker proof. The implementation will probably never be. I agree, I see a few ways that it could go wrong: - Code is proven correct against the specification, but specification is wrong&#x
42.
by fuklief 8y ago
Are you sure on that? It was B method they used afaik.
43.
by fuklief 8y ago
Does anyone in the industry use it ? Does anyone knows for sure that Airbus uses it ?
44.
by fuklief 8y ago
It's more around 1300 euros actually :-) And it's only possible for EU citizens afaik.
45.
by fuklief 8y ago
Considering the close ties of OCaml and Coq, has anyone done some sort of formal verification for Tezos ?
46.
by fuklief 9y ago
How does it compare to CCured ?
47.
Crellvm: Verified Credible Compilation for LLVM(sf.snu.ac.kr)
72 points by fuklief 9y ago|4 comments
48.
by fuklief 9y ago
Some idea for other subs: Computer Science/Maths/Physics should be the most common I think Also https://eprint.iacr.org/ is used a lot for publishing crypto preprints
49.
by fuklief 9y ago
It seems really skewed towards biology publications, is it on purpose ?
50.
Coming Soon: Machine-Checked Proofs in Everyday Development(media.ccc.de)
185 points by fuklief 9y ago|75 comments
51.
by fuklief 9y ago
"Instead I'd produce a restricted C compiler that only accepted constant time programs, and mapped directly to a limited set of machine instructions." How would the compiler knows if the code it's given is constant-time
52.
HACL*: A Verified Modern Cryptographic Library [pdf](eprint.iacr.org)
2 points by fuklief 9y ago|0 comments
53.
Build it Break it Fix it programming contest is starting(builditbreakit.org)
2 points by fuklief 10y ago|0 comments
54.
by fuklief 11y ago
Coq is also used in industry, in particular by Airbus with the CompCert C compiler.
55.
by fuklief 11y ago
It says the translation is correct, is there any proof of that ?