3 ms·

Sounds like it’s mostly lisp. How mathematically correct and proven (in the math sense) is lisp?

by ianai 3y ago

thumbuddy 3y ago
Do you mean what guarantees does Lisp offer? Not sure what you mean.
deleted 3y ago
[deleted]
ravi-delia 3y ago
Depends on the implementation, but SBCL has all the usual suspects to decent precision. The standard specifies branch cuts and such, and I've never heard any complaints. This is just a backbone for array computations, at a lower level than numpy. It's more about JIT-compilation of a small handful of operations than math overall
- alecmg 3y ago
  without knowing much of either, sounds like petalisp to lisp relation is numba to python. Or numba to numpy?
jackdaniel 3y ago
Maxima is implemented in Common Lisp. The language features full numeric tower with bignums and rationals - generally it is a very good language for number crunching.
theLiminator 3y ago
There's nothing that makes lisp mathematically more correct. It might be easier to write correct code in (emphasis on the might). You could say lisp is more elegant though, as everything is an expression and the language is homoiconic.
- matheusmoreira 3y ago
  > the language is homoiconic There's degrees of truth to this. For example, most production lisps will compile functions to native code instead of storing the literal list of expressions. It's easy to manipulate lisp code before that happens but there's certainly a point where the homoiconicity is sacrificed.
eigenspace 3y ago
This is a nonsense question. It's like asking "how mathematically correct and proven is this rock?"
tmtvl 3y ago
If you want to prove your Lisp, you can always boot up ACL2. It was used (for example) to formally verify Buchberger's algorithm: <https://www.sciencedirect.com/science/article/pii/S0747717109001357 https://www.sciencedirect.com/science/article/pii/S074771710...>
- bella001 3y ago
  [dead]
- WanderPanda 3y ago
  How do you even prove a language? I can't even imagine how that would work. Do you maybe have a pointer on where this rabbit hole starts? The one you provided seems more like a deep pocket than an entrance
  - reikonomusha 3y ago
    You would aim to prove properties of the formal semantics of a language, but that requires the language be described in a formal manner. Check out "The Definition of Standard ML" to get a sense of what a (mostly kosher) formal programming language definition might look like.

Sounds like it’s mostly lisp. How mathematically correct and proven (in the math sense) is lisp?

by ianai 3y ago

Sounds like it’s mostly lisp. How mathematically correct and proven (in the math sense) is lisp?

thumbuddy 3y ago

Do you mean what guarantees does Lisp offer? Not sure what you mean.

deleted 3y ago

[deleted]

ravi-delia 3y ago

Depends on the implementation, but SBCL has all the usual suspects to decent precision. The standard specifies branch cuts and such, and I've never heard any complaints. This is just a backbone for array computations, at a lower level than numpy. It's more about JIT-compilation of a small handful of operations than math overall

alecmg 3y ago
without knowing much of either, sounds like petalisp to lisp relation is numba to python. Or numba to numpy?

jackdaniel 3y ago

Maxima is implemented in Common Lisp. The language features full numeric tower with bignums and rationals - generally it is a very good language for number crunching.

theLiminator 3y ago

There's nothing that makes lisp mathematically more correct. It might be easier to write correct code in (emphasis on the might). You could say lisp is more elegant though, as everything is an expression and the language is homoiconic.

matheusmoreira 3y ago
> the language is homoiconic There's degrees of truth to this. For example, most production lisps will compile functions to native code instead of storing the literal list of expressions. It's easy to manipulate lisp code before that happens but there's certainly a point where the homoiconicity is sacrificed.

eigenspace 3y ago

This is a nonsense question. It's like asking "how mathematically correct and proven is this rock?"

tmtvl 3y ago

If you want to prove your Lisp, you can always boot up ACL2. It was used (for example) to formally verify Buchberger's algorithm: <https://www.sciencedirect.com/science/article/pii/S0747717109001357 https://www.sciencedirect.com/science/article/pii/S074771710...>

bella001 3y ago
[dead]
WanderPanda 3y ago
How do you even prove a language? I can't even imagine how that would work. Do you maybe have a pointer on where this rabbit hole starts? The one you provided seems more like a deep pocket than an entrance
- reikonomusha 3y ago
  You would aim to prove properties of the formal semantics of a language, but that requires the language be described in a formal manner. Check out "The Definition of Standard ML" to get a sense of what a (mostly kosher) formal programming language definition might look like.