> Python is Turing complete, but does [TLA,] need to be? Is there an in-Python syntax that can be expanded in place by tooling for pretty diffs; How much overlap between existing runtime check DbC decorators and these modeling primitives and feature extraction transforms should there be? (In order to: minimize cognitive overload for human review; sufficiently describe the domains, ranges, complexity costs, inconstant timings, and the necessary and also the possible outcomes given concurrency,)

From "S2n-TLS – A C99 implementation of the TLS/SSL protocol" https://www.hackerneue.com/item?id=38510025 :

> But formal methods (and TLA+ for distributed computation) don't eliminate side channels. [in CPUs e.g. with branch prediction, GPUs, TPUs/NPUs, Hypervisors, OS schedulers, IPC,]

Still though, coverage-based fuzzing;

From https://www.hackerneue.com/item?id=30786239 :

> OSS-Fuzz runs CloudFuzz[Lite?] for many open source repos and feeds OSV OpenSSF Vulnerability Format: https://github.com/google/osv#current-data-sources

From "Automated Unit Test Improvement using Large Language Models at Meta" https://www.hackerneue.com/item?id=39416628 :

> "Fuzz target generation using LLMs" (2023), OSSF//fuzz-introspector*

> gh topic: https://github.com/topics/coverage-guided-fuzzing

The Fuzzing computational task is similar to the Genetic Algorithm computational task, in that both explore combinatorial Hilbert spaces of potentially infinite degree and thus there is need for parallelism and thus there is need for partitioning for distributed computation. (But there is no computational oracle to predict that any particular sequence of combinations of inputs under test will deterministically halt on any of the distributed workers, so second-order methods like gradient descent help to skip over apparently desolate territory when the error hasn't changed in awhile)

The Fuzzing computational task: partition the set of all combinations of inputs for distributed execution with execute-once or consensus to resolve redundant results.

DbC Design-By-Contract patterns include Preconditions and Postconditions (which include tests of Invariance)

We test Preconditions to exclude Inputs that do not meet the specified Ranges, and we verify the Ranges of Outputs in Postconditions.

We test Invariance to verify that there haven't been side-effects in other scopes; that variables and their attributes haven't changed after the function - the Command - returns.

DbC: https://en.wikipedia.org/wiki/Design_by_contract :

> Design by contract has its roots in work on formal verification, formal specification and Hoare logic.

TLA+ > Language: https://en.wikipedia.org/wiki/TLA%2B#Language

Formal verification: https://en.wikipedia.org/wiki/Formal_verification

From https://www.hackerneue.com/item?id=38138319 :

> Property testing: https://en.wikipedia.org/wiki/Property_testing

> awesome-python-testing#property-based-testing: https://github.com/cleder/awesome-python-testing#property-ba...

> Fuzzing: https://en.wikipedia.org/wiki/Fuzzing

Software testing > Categorization > [..., Property testing, Metamorphic testing] https://en.wikipedia.org/wiki/Software_testing#Categorizatio...

--

From https://www.hackerneue.com/item?id=28494885#28513982 :

> https://github.com/dafny-lang/dafny #read-more

> Dafny Cheat Sheet: https://docs.google.com/document/d/1kz5_yqzhrEyXII96eCF1YoHZ...

> Looks like there's a Haskell-to-Dafny converter.

haskell2dafny: https://gitlab.doc.ic.ac.uk/dcw/haskell-subset-to-dafny-tran...

--

Controlled randomness: tests of randomness, random uniform not random norm, rngd, tests of randomness:

From https://www.hackerneue.com/item?id=40630177 :

> google/paranoid_crypto.lib.randomness_tests: https://github.com/google/paranoid_crypto/tree/main/paranoid... docs: https://github.com/google/paranoid_crypto/blob/main/docs/ran...