recross-coq VS .NET Runtime

I'm currently building a couple of regexp engines:

One, that's a formalization[0] in Coq with big-step semantics, which uncommonly has the intersection operator, and includes several equivalence relations and a proof of the pumping lemma, excepting one case (more on that below).

As a learning exercise and for historical reasons, I've also mostly ported Rust Cox's re1 engine to Rust[1], which includes VM matchers in the style of Henry Spencer, Ken Thompson, and Rob Pike. I also plan to port Doug McIlroy's engine[2], which is interesting for having intersection and complement and special handling for sublanguages, all the way down to just concatenation matched with Knuth-Morris-Pratt. I also want to examine the Rust (thanks burntsushi!), RE2, and Plan 9 engines in more depth.

Once I have time to get back to the project, I want to get back to my regular expression crossword puzzle solver. For that, I'm converting the hint regexps to DFAs, that match strings of some fixed length, and concatenating and intersecting them, until a single regexp is yielded, which should be a string literal, if the puzzle has a single solution. For backreferences, it's more tricky, but I plan on rewriting backreferences to the captured expression, where the lengths of both match, then either executing it with a stack like a pushdown automata or constructing a set of constraints on the characters by index.

As an aside: In my proof of the pumping lemma[3], I got stuck on the case for intersection and I'd love insight. Regular languages are closed under intersection, so the pumping lemma should hold for my implementation. I need to prove that if s =~ re1 and s =~ re2 can be pumped, then so can s =~ And re1 re2. My problem is that re1 and re2 split s into different substrings s = s11 ++ s12 ++ s13 = s21 ++ s22 ++ s23, then state that (forall n, s11 ++ repeat s12 n ++ s13 =~ re1) and (forall n, s21 ++ repeat s22 n ++ s23 =~ re2). My intuition is that s11 = s21, s12 = s22, and s13 = s23, because they both match for the intersection, but I'm not convinced of that and haven't been able to formulate a proof for that.

0: https://github.com/thaliaarchi/recross-coq

.NET has explicit tailcalls - they are heavily used by and were made for F#.

https://learn.microsoft.com/en-us/dotnet/api/system.reflecti...

https://github.com/dotnet/runtime/blob/main/docs/design/feat...

The description indicates it is not production ready, and is archived at the same time.

If you pull all stops in each respective language, C# will always end up winning at parsing text as it offers C structs, pointers, zero-cost interop, Rust-style struct generics, cross-platform SIMD API and simply has better compiler. You can win back some performance in Go by writing hot parts in Go's ASM dialect at much greater effort for a specific platform.

For example, Go has to resort to this https://github.com/golang/go/blob/4ed358b57efdad9ed710be7f4f... in order to efficiently scan memory, while in C# you write the following once and it compiles to all supported ISAs with their respective SIMD instructions for a given vector width: https://github.com/dotnet/runtime/blob/56e67a7aacb8a644cc6b8... (there is a lot of code because C# covers much wider range of scenarios and does not accept sacrificing performance in odd lengths and edge cases, which Go does).

Another example is computing CRC32: you have to write ASM for Go https://github.com/golang/go/blob/4ed358b57efdad9ed710be7f4f..., in C# you simply write standard vectorized routine once https://github.com/dotnet/runtime/blob/56e67a7aacb8a644cc6b8... (its codegen is competitive with hand-intrinsified C++ code).

There is a lot more of this. Performance and low-level primitives to achieve it have been an area of focus of .NET for a long time, so it is disheartening to see one tenth of effort in Go to receive so much spotlight.

It's an interesting "time is a circle" problem given that a century only has 100 years and then we loop around again. 2-digit years is convenient for people in many situations but they are very lossy, and horrible for machines.

It reminds me of this breaking change to .Net from last year.[1][2] Maybe AA just needs to update .Net which would pad them out until the 2050's when someone born in the 1950s would be having...exactly the same problem in the article. (It is configurable now so you could just keep pushing it each decade, until it wraps again).

Or they could use 4-digit years.

[1] https://github.com/dotnet/runtime/issues/75148

These can also be passed as arguments to `dotnet publish` if necessary.

Reference:

- https://learn.microsoft.com/en-us/dotnet/core/deploying/nati...

- https://github.com/dotnet/runtime/blob/main/src/coreclr/nati...

- https://github.com/dotnet/runtime/blob/5b4e770daa190ce69f402... (full list of recognized keys for IlcInstructionSet)

Yes, that is true. I'm not sure about JVM implementation details but the reason the comment says "virtual and interface" calls is to outline the difference. Virtual calls in .NET are sufficiently close[0] to virtual calls in C++. Interface calls, however, are coded differently[1].

Also you are correct - virtual calls are not terribly expensive, but they encroach on ever limited* CPU resources like indirect jump and load predictors and, as noted in parent comments, block inlining, which is highly undesirable for small and frequently called methods, particularly when they are in a loop.

* through great effort of our industry to take back whatever performance wins each generation brings with even more abstractions that fail to improve our productivity

[0] https://github.com/dotnet/coreclr/blob/4895a06c/src/vm/amd64...

[1] https://github.com/dotnet/runtime/blob/main/docs/design/core... (mind you, the text was initially written 18 ago, wow)

If you care about portable SIMD and performance, you may want to save yourself trouble and skip to C# instead, it also has an extensive guide to using it: https://github.com/dotnet/runtime/blob/69110bfdcf5590db1d32c...

CoreLib and many new libraries are using it heavily to match performance of manually intensified C++ code.

DEBUG: packageFiles with updates (repository=local) "config": { "nuget": [ { "deps": [ { "datasource": "nuget", "depType": "nuget", "depName": "Microsoft.Extensions.Hosting", "currentValue": "7.0.0", "updates": [ { "bucket": "non-major", "newVersion": "7.0.1", "newValue": "7.0.1", "releaseTimestamp": "2023-02-14T13:21:52.713Z", "newMajor": 7, "newMinor": 0, "updateType": "patch", "branchName": "renovate/dotnet-monorepo" }, { "bucket": "major", "newVersion": "8.0.0", "newValue": "8.0.0", "releaseTimestamp": "2023-11-14T13:23:17.653Z", "newMajor": 8, "newMinor": 0, "updateType": "major", "branchName": "renovate/major-dotnet-monorepo" } ], "packageName": "Microsoft.Extensions.Hosting", "versioning": "nuget", "warnings": [], "sourceUrl": "https://github.com/dotnet/runtime", "registryUrl": "https://api.nuget.org/v3/index.json", "homepage": "https://dot.net/", "currentVersion": "7.0.0", "isSingleVersion": true, "fixedVersion": "7.0.0" } ], "packageFile": "RenovateDemo.csproj" } ] }

https://github.com/dotnet/runtime/issues/59591

Support zstd Content-Encoding:

We might not be that far away already. There is this issue[1] on Github, where Microsoft and the community discuss some significant changes.

There is still a lot of questions unanswered, but initial tests look promising.

Ref: https://github.com/dotnet/runtime/issues/94620