Temporal SVC (reduce framerate if bandwidth constrained) is pretty widely supported by now, right? Though maybe not for H.264, so it probably would have scaled nicely but only on Webrtc?

    $x$.foo($args$)

You can also access the full intellij API via groovy scripts in the filters or when computing replacement variables, if you really want.

Though most of the time built in refactors like 'extract to _' or 'move to' or 'inline' or 'change type signature' or 'find duplicates' are enough.

If an expression might be unused, throw a closure which computes it on the heap

If the value is actually needed, invoke the closure. Optionally replace the closure with a black hole. A black hole is just a closure which pauses any thread which calls it, to be resumed once the first thread finishes with the expression

Once finished, replace with a closure which immediately returns the computation result. (Or often save the indirection because most concrete values also act as closures which immediately returns themselves using info table pointers trickery)

Anyway, iirc WasmGC wants very rigid types without dynamic type changes. Extra indirections could fix that, Oor maybe defunctionalizing thunks into a tagged union, but both sound expensive. Especially without being able to hook into the tracing step for indirection removal.

Also, Haskell supports finalizers so WasmGC would need that as well.

Like, if you have a constraint is_even(x) that's really easy to check in your head with some informal Floyd-Hoare logic.

And it scales to extracting code into helper functions and multiple variables. If you must track which set of variables form one context x1+y1, x2+y2, etc I find it much harder to check the invariants in my head.

These 'fixed state shape' situations are where I'd grab a state monad in Haskell and start thinking top-down in terms of actions+invariants.

Though storing the data locally still could make getting compromised by a targeted attack more dangerous.

A computation graph which gets sampled like here is much slower but can be accurate. You don't need an abstract domain which loses precision at every step.

The most interesting case is implicit scope+non-tail recursion, usually this requires you to capture the variable context in mutable objects/monads/effects or similar.

This explicit capturing is neat because you still have consistent shapes for your state to define invariants over, but it's easier to decompose the logic and ignore parts of the context which are irrelevant. It lets you split problems into domain specific languages, each of which has a set of (maybe overlapping) contexts, and ideally each of which can be proven in isolation.

Also, the control flow of loops is a very restricted case of even tail jumps. Tail recursion has arbitrary jumps between basic blocks and loops are properly nested basic blocks. Even with labeled breaks, efficiently simulating arbitrary tail recursion without goto is tough. Induction proofs/data flow analysis/abstract interpretation don't care, but I'm not sure it makes proofs easier.

Requires the language to have something equivalent to pattern synonyms to be as invisible as twee, though.

In twee a TermList is a slice of a bytearray (two ints for offset/length plus a pointer).

And a term is an int for the function symbol and an unpacked TermList for the arguments.

The pattern match synonyms load a flat representation from the array into a view type, and the allocation of the view type cancels out with the pattern matching so everything remains allocation free.

https://hackage.haskell.org/package/twee-lib-2.4.2/docs/Twee...

Which is fun, because correct highlighting depends on language version. Haskell has similar problems where different compiler flags require different parsers. Close enough is sufficient for syntax highlighting, though.

Python is also a bit weird because it calls the format methods, so objects can intercept and react to the format specifiers in the f-string while being formatted.

From the python 3.6 change log:

New dict implementation¶ The dict type now uses a “compact” representation based on a proposal by Raymond Hettinger which was first implemented by PyPy. The memory usage of the new dict() is between 20% and 25% smaller compared to Python 3.5.

The order-preserving aspect of this new implementation is considered an implementation detail and should not be relied upon (this may change in the future, but it is desired to have this new dict implementation in the language for a few releases before changing the language spec to mandate order-preserving semantics for all current and future Python implementations; this also helps preserve backwards-compatibility with older versions of the language where random iteration order is still in effect, e.g. Python 3.5). (Contributed by INADA Naoki in bpo-27350. Idea originally suggested by Raymond Hettinger.)

https://docs.python.org/3.6/whatsnew/3.6.html#new-dict-imple...

As the other comment mentioned pcre-compatible Regex are a standard, though the pcre spec isn't super readable. There are some projects that have more readable docs like mariadb and PHP, but it doesn't really make sense to repeat the spec in library docs https://www.php.net/manual/en/regexp.reference.unicode.php

There are libraries for pcre2 or gnu regex syntax with the same API if you prefer those

    > import Control.Regex.Lens.Text
    > "Foo, bar" ^.. [regex|\p{L}+|] . match
    ["Foo", "bar"]
    > "Foo, bar" & [regex|\p{L}+|] . ix 1 . match %~ T.intersperse '-' . T.toUpper
    "Foo, B-A-R" 

    import OpenSSL.Session (context)
    import Network.HTTP.Client.OpenSSL

    let opts = defaults & manager .~ Left (opensslManagerSettings context)
    withOpenSSL $
      getWith opts "https://httpbin.org/get"

To do this chasing precisely you need some metadata, saying which fields are pointers vs other data like ints. For OOP languages this metadata is stored with the vtables for objects. For the stack you need similar metadata, at the very least how many pointers there are if you put them first in the stackframe.

Not having this metadata and conservatively treating random ints as pointers isn't always catastrophic, but it has some drawbacks. Two big ones:

- a moving GC is tough, you have to update pointers after moving an object but can't risk updating random ints that happen to have that value

- You do more work during GC chasing random non-pointers, and free less memory meaning more GC runs

Generating ths precise GC metadata for stackframes is sort-of easy.You need specific Safe-Points where all data is at known locations for the GC to work anyway, usually by spilling resgisters to the stack. These GC checkpoints usually coincide with heap allocation, which is why long non-allocating loops can block stop-the-world GC and send other threads into a spin-lock in many GC implementations

Maybe a non-precise GC could treat registers as possible pointers and skip spilling to the stack for Safe-Points? There are alternatives to spilling like a precise stack-map for each program instruction (so every instruction is a safe point), but those are expensive to process. Usually only used for debugging or exception handling, not something frequent like GC

Similar to the algorithm to parallelize the merge step of merge sort. Split the two sorted sequences into four sequences so that `merge(left[0:leftSplit], right[0:rightSplit])+merge(left[leftSplit:], right[rightSplit:])` is sorted. leftSplit+rightSplit should be halve the total length, and the elements in the left partition must be <= the elements in the right partition.

Seems impossible, and then you think about it and it's just binary search.

- memoization sometimes crucial for performance.

- passing objects and functions around is common.

- you cannot compare objects and functions for semantic equality

If you wrote larger react apps you almost certainly had to useCallback at some point so that memoization worked, the compiler fixes that.

Whenever you construct an object or function the react compiler memoizes on their free variables so pointer equality is sufficient.

Though I do think the compiler caches too aggressively, even if there are no free variables and hoisting is sufficient or escape analysis shows it is unnecessary for semantics.

You already use tons of solvers because proving everything by hand is mind numbingly tedious and time consuming, but tactics/solvers really struggle if you throw too many theorems and lemmas at them. Neural nets as search machines to pattern match relevant lemmas fit perfectly. Similarly induction and higher order unification are full-on code synthesis where brute-force iterating over all possible syntax trees is really inefficient.

And solvers do a backtracking solve anyway, so if the ai returns 95% irrelevant lemmas it doesn't matter. Still would be a dramatic improvement over manually searching for them.

Though I'm not convinced that computer checked proofs are necessarily good for communication. There are reasons beside page-count that proofs for human consumption are high-level and gloss over details.

Monads are types that let you build chains of lambdas, so you can mix control flow and variable scoping with the some type-specific logic.

Async IO/streams/optionals are monads. It's no accident that these could be programmed as nested callbacks/nested loops/nested if statements. That's the nested chain of Monad->lambda->Monad->...

Monads work well with syntax sugar (think async/await), and some languages like Haskell can abstract over them in neat ways.