ZoltanAK2's comments

YMMV, but Austral-lang (https://austral-lang.org/) comes quite close to what I want out of a smaller, simpler, safer Rust.

Its syntax is inspired by Ada, and as far as I know the designer has no PhD in type theory, so it matches the requirements put forth by the other commenters too.

You write, "we shouldn't need the axiom of choice to define the derivative."

The good news is that we don't!

Only model-theoretic approaches, which justify the infinitesimal methods by constructing a hyperreal field, require (a weak form of) the axiom of choice [2].

However, there are axioms for nonstandard analysis which are conservative over the usual choice-free set theory ZF. The three axioms of Hrbacek and Katz presented in the article "Infinitesimal analysis without the Axiom of Choice" [1] are the best recent example: these axioms allow you to do everything that is done in Keisler's book and more (including defining the derivative), and you never need to invoke the axiom of choice to justify them.

[1] https://arxiv.org/abs/2009.04980

[2] Essentially, the set of properties satisfied by a fixed nonstandard hypernatural gives rise to a non-principal ultrafilter over the naturals. The axiom of choice is necessary to prove the existence of non-principal ultrafilters in (choice-free) set theory, but the existence of non-principal ultrafilters is not sufficient to prove the axiom of choice.

Indeed, the linear type systems makes sure that you won't forget to dispose of resources.

Linear types enable manual memory management without memory leaks, use-after-free, double free errors, garbage collection, or any runtime overhead in either time or space other than having an allocator available. More generally, it enables us to manage any resource (file handles, socket handles, etc.) that has a lifecycle without letting us forget to dispose of the resource (e.g. leaving a file handle open), dispose of it twice, or use it after disposal (e.g. reading from a closed socket), all without runtime overhead.

The Austral tutorial's chapter on linear types (https://austral-lang.org/tutorial/linear-types) explains how this works in a fairly clear way.

There is discrepancy because things the programmer can prevent are handled differently from things the programmer cannot prevent.

The programmer can always statically ensure that the program doesn't experience a trapped overflow, and that the stack size is not exceeded. All the information to do that is available when the programmer runs the compiler.

But there is no way to prevent a memory allocation failure when using `calloc`, since the information required to do that is not available when the programmer writes the code. In fact, when running on POSIX systems it's not even possible to check _in advance_ at runtime whether a memory allocation will succeed.

This is why Austral's allocateBuffer(count: Index): Address[T] returns an Address[T], which you have to explicitly null-check at run-time (and the type system ensures that you can't forget to do this).

Of course, on some non-POSIX systems such as seL4, the programmer can know at compile-time that memory allocations (untypedRetype) will not fail. When you use Austral on such systems, you don't have to use calloc/allocateBuffer at all.

In accordance with the 'scuttle the ship' philosophy, Austral programs abort immediately when trapping arithmetic overflows, with the message "Overflow in trappingOpname (TypeName)".

Almost certainly not, and there are good reasons for that.

Work on Austral was initiated by Borretti in 2021, but its earnest development really only commenced in January this year. So we're talking about a language that's, for most intents and purposes, less than a year old. Even if the January release was stable, there would not have been time for anyone to develop and deploy significant projects in it. But it is not stable: it still under construction, with certain inherent instabilities. Notably, recent updates changed the borrow syntax and FFI pragmas. Similarly, the surrounding infrastructure (compiler and standard library) is far from production-ready yet.

I built an Austral interface for the seL4 Core Platform (https://github.com/zaklogician/libmantle/tree/main), and ran some Austral apps on hardware. The purpose of this was experimental (we wanted to know how Austral can help us design fail-safe seL4 Core Platform APIs, and it was a success), but probably among the closest anybody came to "production": I wrote more Austral code than currently included in the Austral standard library.

It revealed several bugs, including a typo in Standard.Buffer which leads to the invariant check for the Buffer type always failing, and issues related to the compiler's handling of large unsigned literals.

Austral shows great promise, and has already provided us with valuable insights about linear API design, and exciting glimpses into its future capabilities. Using Austral in production code, however, might require a few more years of maturation and stabilization. So if you want something that people use for writing production code, check back in a couple of years.

Ultimately, the taxpayer funds the researchers' salaries, and the researchers spend some of their research time on peer review instead of advancing their research.

But these hours dedicated to peer review are not the issue: something scientifically useful gets done. It's the tax dollars that go to Elsevier, in exchange for literally nothing*, that we should worry about.

* sometimes they charge you, the taxpayer, in exchange for access to the research output

> They also manage the review process (screen papers, find reviewers, communicate with authors and reviewers),

They do not. That's the editor's job, and Elsevier journal editors are unpaid volunteers -- as the Guardian article correctly pointed out.

> A half-decent review can easily take 3-4 hours, and a typical paper gets 2-3 reviews, so something like 8-12 hours of PhD-level labor which are not currently compensated.

It generally takes much much longer than that.

The average article in Neuroimage is 14 pages long (~ 10000 words), not counting references and declarations. Pure reading, single-domain, technical: the chart says 10k words will take at least 60 minutes. And you'll definitely need to read the article more than once while doing peer review.

Then you'll need to look up references, do some sanity check calculations, evaluate artifacts if available, scrutinize figures, and unless you're up-to-date on all recent developments of the field, probably read at least one more article on prior work just to understand what's going on. If unusual methods were used in the evaluations, you have to understand these too, so better add a few more days.

And you still have to actually write the review: at that point, you only have some notes and scribbles! In neuroscience, we're talking about at least 2-3 days of FTE work. And that's only the first round of reviews. About 80% of articles go through multiple rounds of review-response, according to Neuroimage's own statistics.

In other fields, review times might be significantly longer (weeks, or in mathematics even months, instead of days).

Elsevier profit margins are 40%, according to their own admission. They could afford the costs of compensating this labor. But why would they?

Cantor space is just the space formed by infinite binary sequences, that is sequences which assumes only the values 0 or 1.

Considered as a topological space, Cantor space happens to have the same structure as the Cantor set, a highly disconnected subset of the real numbers that has some at-first-unintuitive properties.

But you don't have to understand, or even worry about this correspondence to grasp what's going on with seemingly impossible functional programs. Thinking about Cantor space as "the type of infinite binary sequences" is good enough.

At one point during my PhD, I proved a fairly technical theorem, which generalized a result from 1996. Both my result and the 1996 result used techniques from nonstandard analysis.

About 6 months later, an article appeared on arXiv, and pointed out that the 1996 proof had a flaw in it (fortunately, the result did hold, but the proof required some modification).

I felt terrified: I was using very similar techniques, but as part of a more complicated proof. I couldn't guarantee that I didn't make a similar (or worse) mistake. So I sat down with the Agda proof assistant, and wrote about 4000 lines of code to verify the theorem I proved (Agda differs from ACL2 quite a bit, and I ended up developing an extension to Martin-Löf type theory so that I could formalize this style of reasoning effectively).

This reassured me that my result was correct, and it made for a nice chapter in my thesis. And it convinced me that nonstandard analysis synergizes very effectively with both automated and interactive theorem proving.

Nonstandard analysis helps automated theorem proving by keeping quantifier complexity [1] low. Statements that have many quantifier alterations. Statements that have many alterations of quantifiers are more difficult to handle than ones with fewer quantifier alterations: young children can frequently grasp the definition of monotonicity (no quantifier alterations, "for all x and y, ..."), but they have a much harder time with continuity (2 quantifier alterations, "for all x and for all ε, there is some δ such that for all y"). The same holds for machines: they have a much easier time if quantifier complexity is kept low. Nonstandard analysis accomplishes that in many settings: for example, you can use it to express continuity without quantifier alterations.

Nonstandard analysis helps interactive theorem proving in multiple ways. Just like in automated theorem proving, it lowers quantifier complexity, and it makes it easier to express certain definitions. But nonstandard analysis also improves "code reuse": certain combinatorial theorems imply their "infinite counterparts" via a few lines of nonstandard analysis. This is not that important or useful in informal, pen-and-paper mathematics, since the finite and the infinite theories developed in parallel, and tend to be equally developed as a result. But it comes in handy when we do interactive theorem proving: some areas of mathematics have not been formalized yet, and formalizing all the bits of "infinite" theory that you need for your result may take a long time. In many cases, a tiny bit of nonstandard analysis can help us sidestep such issues.

Synergy goes both ways, in that interactive theorem proving helps nonstandard analysis too. There are very few people who are familiar with the techniques of nonstandard analysis, so it can be hard to find people who can proof-read or referee new works. And since nonstandard analysis (both the IST formalism used in the linked article and the model-theoretic approach) relies on syntactic restrictions, accidental mistakes in nonstandard analysis proofs have a distinct "flavor", different from most other areas of mathematics. This means that reviewing requires a bit more care than usual. Proof assistants and proof checkers are incredibly useful here.

[1] https://mathoverflow.net/questions/281894/examples-of-statem...