log☇︎
21 entries in 0.405s
diana_coman: ah, not with the standard, ofc not; with whatever certificate x measures (as they say: traceability, formal verification, stack consumption)
a111: Logged on 2018-04-11 04:05 ckang: sorta related, but what do you think about this.. https://www.wireguard.com/papers/wireguard-formal-verification.pdf
spyked: http://btcbase.org/log/2018-04-11#1796332 <-- but one can, by reading the orig. paper, decompose it into windowses that then can be replaced, e.g. http://trilema.com/2016/the-necessary-prerequisite-for-any-change-to-the-bitcoin-protocol/ . granted, it took me years to peel off the layers of understanding and I'm still not quite there yet, but this is completely different from $formal_verification_devoid_of_meaning. ☝︎
a111: Logged on 2018-04-11 04:05 ckang: sorta related, but what do you think about this.. https://www.wireguard.com/papers/wireguard-formal-verification.pdf
asciilifeform: with generous helpings of c pointerolade, opensslism, mathemadturbatorily- squigglymarked pdfolade, tall claims of 'formal verification', etc
a111: Logged on 2018-04-11 04:06 ckang: https://www.wireguard.com/formal-verification/
mircea_popescu: the fundamental problem with formal verification is that it's not currently implemented seriously (which is to say -- completely, on small codebases). it's just machines poking at things generally, in an untenable theoretical model.
a111: 12 results for "formal verification", http://btcbase.org/log-search?q=formal%20verification
mircea_popescu: !#s formal verification
ckang: https://www.wireguard.com/formal-verification/ ☟︎
ckang: sorta related, but what do you think about this.. https://www.wireguard.com/papers/wireguard-formal-verification.pdf ☟︎☟︎
asciilifeform: re 'formal verification', what a lol
spyked: the whole thing is. and yes, this is "formal verification 101" taught in universities. if you want to get even more outraged about it, read Heiser's post at the beginning.
mircea_popescu: i thought that's done automatically already, in formal verification
a111: Logged on 2017-07-13 15:06 phf: and they are coming from the "formal verification" direction, via spark
phf: and they are coming from the "formal verification" direction, via spark ☟︎
herbijudlestoids: asciilifeform: I didn't look too deeply, but take a look, it has TLA+ style formal verification properties
mats: yes, and if you reject a inputs outside of a defined set of formal-izable grammars, the more constrained the model and subsequently greater approachability towards program verification
benkay: cads: what kind of factory worker reads about formal verification of large software projects?!
cads: The issue I see with formal verification is so few people know to ask for it by name
cads: I'm thinking risk and externalities on the insurance derivative over this kind of service would be _far_ beyond my abilities to manage. However a code review would be quite lucrative and low risk. Also, it might be reasonable to begin offering formal verification services from the gate, or about 1 year after startup. It's not that hard to teach. When you have your own slaves.