21 entries in 0.299s
: ah, not with the standard, ofc not; with whatever certificate x measures (as they say: traceability, formal verification
, stack consumption)
: with generous helpings of c pointerolade, opensslism, mathemadturbatorily- squigglymarked pdfolade, tall claims of 'formal verification
: 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.
: 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.
: i thought that's done automatically already, in formal verification
: Logged on 2017-07-13 15:06 phf: and they are coming from the "formal verification
" direction, via spark
: and they are coming from the "formal verification
" direction, via spark ☟︎
: asciilifeform: I didn't look too deeply, but take a look, it has TLA+ style formal verification
: 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
: cads: what kind of factory worker reads about formal verification
of large software projects?!
: The issue I see with formal verification
is so few people know to ask for it by name
: 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.