I read the entire manifesto thinking the discourse about a code execution model would lead to a revelation that this is a model that can reduce bugs in code in realtime and make sure the code runs to the original spec or blueprint. Instead it turned out to be about a model that keeps on optimising code that can go faster and faster over time. That's very exciting in its own right, don't get me wrong, but I was really starting to hope this would be about creating code that breaks less etc.

Maybe it means both but perhaps the emphasis is on speed.

▲

f0e4c2f7 16 hours ago | parent | next [-]

For the first thing you're talking about check out bend.

https://github.com/bendlang/bend

	▲	laginimaineb 6 hours ago \| parent \| next [-]
		Bend is a formal language, but its use is quite different (also, Bend is much too narrow for Maxwell's use case...). We need proofs of equivalence (including for code with side effects!) between original code, and new code, possibly in some other language. Say Python and a raw SIMD implementation. To do this we have a full 'embedding' of said languages in the same formal framework. It also requires modeling exactly what 'state' means in dynamic high level languages.
	▲	krmmalik 8 hours ago \| parent \| prev [-]
		Thanks!

▲

laginimaineb 16 hours ago | parent | prev [-]

Yes, CEMs can also help reduce bugs. To give an example, we found several memory safety bugs in core CPython code, through our formalisation. We'll release more details on that soon.