|
Jonathan Protzenko
@
_protz_
Seattle, WA
|
|
Formal verification, cryptography, type systems, and stuff
|
|
|
282
Tweetovi
|
211
Pratim
|
427
Osobe koje vas prate
|
| Tweetovi |
| Jonathan Protzenko proslijedio/la je tweet | ||
|
Laurent Joubert
@ljo
|
6 h |
|
Excellent work presented today at @Etalab by Denis Merigoux. Check gitlab.inria.fr/verifisc/verif… under #GPLv3 #bluehats. All this was enabled thanks to the open source code of tax code by @dgfip_officiel pic.twitter.com/NW9GER7CLV
|
||
|
|
||
|
Jonathan Protzenko
@_protz_
|
31. sij |
|
|
||
|
Jonathan Protzenko
@_protz_
|
31. sij |
|
Made it to DC. Couldn't get a ticket to attend the impeachment so I'll stick with @shmoocon instead.
|
||
|
|
||
|
Jonathan Protzenko
@_protz_
|
31. sij |
|
Of course. It's better than nothing. But my hope is that i) such in-house solutions can become more open and ii) either the administration engages with research / PL / etc. or establishes in-house research-aware experts.
|
||
|
|
||
|
Jonathan Protzenko
@_protz_
|
31. sij |
|
But jokes aside it's absolutely abominable. They need to execute the whole thing repeatedly to get it to converge.
|
||
|
|
||
|
Jonathan Protzenko
@_protz_
|
31. sij |
|
You have no respect for your motherland and its glorious administration. France!
|
||
|
|
||
|
Jonathan Protzenko
@_protz_
|
31. sij |
|
Denis is wise and is not on Twitter. But I'll be forwarding to him the oh-so-vital "tweet impression statistics" and whatnot.
|
||
|
|
||
|
Jonathan Protzenko
@_protz_
|
31. sij |
|
The corresponding research article, alas, is only in French: hal.inria.fr/hal-02320347v3… time to brush up your skills and parler français
|
||
|
|
||
|
Jonathan Protzenko
@_protz_
|
31. sij |
|
My student Denis wrote a formal semantics for the French tax code, complete with Coq proof of soundness and SMT queries to uncover unfair tax hikes. PL for fiscal justice! blog.merigoux.ovh/en/2019/12/20/…
|
||
|
|
||
|
Jonathan Protzenko
@_protz_
|
24. sij |
|
For all your cryptographic needs (ahem, e.g., HACL*) use a formally verified, constant time-preserving C compiler! @davidpichardie at #popl pic.twitter.com/kN4JTOxkT9
|
||
|
|
||
|
Jonathan Protzenko
@_protz_
|
22. sij |
|
Thanks to all who attended and contributed thoughts and conversation to HASE 2020 and made it a great workshop! Now on to #popl2020 pic.twitter.com/pGSpmli8uY
|
||
|
|
||
|
Jonathan Protzenko
@_protz_
|
8. sij |
|
Too many lambdas in your POPL program? Consider registering for HASE popl20.sigplan.org/home/hase-2020! You'll even get to meet the mythical "practitioner" in a laid-back, interactive setting with an audience-driven agenda...!
|
||
|
|
||
| Jonathan Protzenko proslijedio/la je tweet | ||
|
Nadim Kobeissi
@kaepora
|
29. pro |
|
Now at #36C3, @hashbreaker and @hyperelliptic talk about EverCrypt and formally verified cryptographic primitives, promoting formally verified crypto as the future for software implementations. pic.twitter.com/rfhtToswbK
|
||
|
|
||
| Jonathan Protzenko proslijedio/la je tweet | ||
|
ShmooCon
@shmoocon
|
19. pro |
|
What to know who will be talking about what? Check out the 2020 list of speakers here: shmoocon.org/2019/12/19/shm…
|
||
|
|
||
|
Jonathan Protzenko
@_protz_
|
13. pro |
|
* start. I had proofread this twice 😭
|
||
|
|
||
|
Jonathan Protzenko
@_protz_
|
13. pro |
|
New blog post! GitHub strange, or the weird repositories you find when you starting digging into commit data... with a cameo appearance by @avsm jonathan.protzenko.fr/2019/12/08/git…
|
||
|
|
||
| Jonathan Protzenko proslijedio/la je tweet | ||
|
Boris
@bz_moz
|
10. pro |
|
When someone's bonus or promotion depends on them shipping a "spec" or a feature, it's hard for them to accept feedback that the whole thing is a bad idea and should be dropped.
|
||
|
|
||
| Jonathan Protzenko proslijedio/la je tweet | ||
|
Paul Krugman
@paulkrugman
|
7. pro |
|
Yes, French GDP has grown more slowly than GDP here. Much of that is slower population growth. And you do need to ask, growth for whom. Most French live *better* than their US counterparts 2/ voxeu.org/article/econom… pic.twitter.com/bZHydwLxM1
|
||
|
|
||
|
Jonathan Protzenko
@_protz_
|
27. stu |
|
Congratulations @zx2c4! Thrilled to see verified cryptography finally landing in the Linux kernel. It's been a long road, but hopefully follow-ups will be easier. twitter.com/EdgeSecurity/s…
|
||
|
|
||
| Jonathan Protzenko proslijedio/la je tweet | ||
|
Edge Security
@EdgeSecurity
|
27. stu |
|
Now that Frankenzinc has landed, v1 of the WireGuard patchset has been submitted upstream to Linux: lkml.org/lkml/2019/11/2… lkml.org/lkml/2019/11/2…
|
||
|
|
||