allocating 15000 gc objects and then seeing them getting freed in a big chunk is about as slow as malloc()ing those same 15000 objects and manually free()ing them when they fall out of scope
just because the sawtooths are microscopic with malloc() doesn't mean they don't exist
as always the real problem is the code that allocates 9 octillion vector3 on the heap
this is a specific trick in the "use mutation so you don't have to allocate 60 gigabytes per second" class of gc-aware program optimizations
fully manual languages are often incredibly painful to do complicated data structures in and eventually you will end up making a minor mistake
it probably makes sense to think like this, until you try doing it, inevitably fuck up, and realize a fundamental truth:
Managing lifetimes in a sufficiently complex program is no simple feat. Accessing a region of memory after it was freed (use-after-free) can severely fuck your shit up. If you leave a "dangling" pointer pointing to a freed region, that region is free to be re-allocated and overwritten with arbitrary data. If an attacker is skilled enough, he can put specially crafted data in one of these regions and have the program access specific chunks of it. A lot of damage can be done this way.
Is there a non-asinine way to safeguard pointers and avoid unwanted memory leakage like this? Such as "unless this pointer's contents is verified to not cause harm and it's actually not being used, zero it and use it", or is it bad for performance?
this general idea is sometimes referred to as "garbage collection"
There are tools to test for memory problems, such as valgrind. Of course, there's no guarantee you will catch them all in testing. Any sort of built-in protection/prevention measure is essentially just one or more of the other memory management paradigms (e.g. ref counting).
Used Coq as well albeit for formalizing mathematics specifically linear algebra. Wanted to try doing the same with C programs and was wondering if there are any good resources on that.
If I'm understanding the question correctly, maybe look into Hoare logic.
if you are managing it yourself:
true, it usually does need a good bit of extra memory to work well, and java limiting the max heap is sort of weird
maybe, but do you actually really know how your modern malloc() implementation works? and do you really want to have the complexity of manually allocating and deallocating every single piece of memory you ever use, just to avoid the complexity of a weird algorithm that walks through your heap every now and then?
and it can do stuff like defragment the heap transparently and allocate and deallocate memory chunks faster than malloc in many scenarios
I like Coq for mathematics as well, but when it comes to programming language verification, the foundational (no pun intended) texts there are the Software Foundations series, specifically Volumes 2 and 5. From my experience most dedicated Coq courses at universities eventually go into DSL verification, and IIRC the INRIA developers themselves lean mostly into language verification instead of mathematics, with the latter being an independent effort by the academic community on top of the system. There is also CompCert, a formally verified compiler for (a significant subset of) C, which seems more directly related to your interest (source available though sadly not free software so beware)
-- agda-unimath snippet
unlabeled-structure-species-types :
{l1 l2 : Level} (F : species-types l1 l2) → ℕ → UU (lsuc l1 ⊔ l2)
unlabeled-structure-species-types {l1} {l2} F n =
Σ ( Type-With-Cardinality-ℕ l1 n)
( λ X → F (type-Type-With-Cardinality-ℕ n X))
https://en.cppreference.com/w/c <- behold: the fucking manual (read it)