Get real-time insights from all types of time series data with InfluxDB. Ingest, query, and analyze billions of data points in real-time with unbounded cardinality. Learn more →
Top 7 Standard ML sml Projects
-
InfluxDB
Power Real-Time Data Analytics at Scale. Get real-time insights from all types of time series data with InfluxDB. Ingest, query, and analyze billions of data points in real-time with unbounded cardinality.
-
WorkOS
The modern identity platform for B2B SaaS. The APIs are flexible and easy-to-use, supporting authentication, user identity, and complex enterprise features like SSO and SCIM provisioning.
https://github.com/MLton/mlton/issues/473
Is there sufficient use of MLTon "native" backend out there to consider it mature? or Do people prefer the LLVM or C backend instead in general?
Project mention: The Deep Link Equating Math Proofs and Computer Programs | news.ycombinator.com | 2023-10-11If I understand what you are asking about correctly, then I do think you are mistaken.
As a sibling comment observed, you would be proving something about a program, but proving things about programs is both possible and done.
This ranges from things like CakeML (https://cakeml.org/) and CompCert (compilers with verified correctness proofs of their optimizations) to something simple like absence of runtime type errors in statically strongly soundly-typed languages.
Of note is that you are proving properties of your program, not proving them perfect in every way. The properties of your program that you prove can vary wildly in both difficulty and usefulness. A sufficiently advanced formally verified compiler like CakeML can transfer a high-level proof about your source code to a corresponding proof about the behavior of the generated machine-executable code.
I'm one of the authors of this work -- I can explain a little.
"Provably efficient" means that the language provides worst-case performance guarantees.
For example in the "Automatic Parallelism Management" paper (https://dl.acm.org/doi/10.1145/3632880), we develop a compiler and run-time system that can execute extremely fine-grained parallel code without losing performance. (Concretely, imagine tiny tasks of around only 10-100 instructions each.)
The key idea is to make sure that any task which is *too tiny* is executed sequentially instead of in parallel. To make this happen, we use a scheduler that runs in the background during execution. It is the scheduler's job to decide on-the-fly which tasks should be sequentialized and which tasks should be "promoted" into actual threads that can run in parallel. Intuitively, each promotion incurs a cost, but also exposes parallelism.
In the paper, we present our scheduler and prove a worst-case performance bound. We specifically show that the total overhead of promotion will be at most a small constant factor (e.g., 1% overhead), and also that the theoretical amount of parallelism is unaffected, asymptotically.
All of this is implemented in MaPLe (https://github.com/mpllang/mpl) and you can go play with it now!
Standard ML sml related posts
- MPL: Automatic Management of Parallelism
- Flunct: Well-typed, fluent APIs in SML
- A good dependency manager for a new programming language?
- Millet, a Language Server for SML
- Modules: Overcoming Stockholm and Duning-Kruger
- Coalton: How to Have Our (Typed) Cake and (Safely) Eat It Too, in Common Lisp
- Standard ML [PLDI 2021]
-
A note from our sponsor - InfluxDB
www.influxdata.com | 26 Apr 2024
Index
What are some of the best open-source sml projects in Standard ML? This list will help you:
Project | Stars | |
---|---|---|
1 | mlton | 916 |
2 | cakeml | 912 |
3 | mpl | 285 |
4 | smlpkg | 157 |
5 | install-mlkit | 5 |
6 | smlnj-viscomp-example | 4 |
7 | sml-parseq | 4 |
Sponsored