xuq01
  • Member for 4 years, 11 months
  • Last seen more than a month ago
  • Japan
Do any programming languages use general recursive functions as their basis?
Accepted answer
45 votes

Direct answer to the question: yes, there are esoteric and highly impractical PLs based on $\mu$-recursive functions (think Whitespace), but no practical programming language is based on $\mu$-...

View answer
What are the concequences of the unit type and the unit value being the same?
Accepted answer
6 votes

You have been confused by Haskell's notation. The unit type and unit value are of course different, and it just happens that Haskell uses the same notation for both. As for the consequences: there ...

View answer
How CompCert "proves" different things in its codebase
Accepted answer
6 votes

I am not very sure what you are asking, and I am also not sure that you have the background to understand CompCert. It seems that you are still confused by some basic concepts in Coq. I would suggest ...

View answer
An example of something you can formally verify with proofs in Software Development
5 votes

Quite a lot of things can and have been formally verified with formal methods. Compilers. We want to prove that a compiler preserves the semantics of its source program. For example, if we write a ...

View answer
What is a fixpoint?
4 votes

Formal definition: a fixed point of a function $g : D \rightarrow D$ is an element $d : D$ such that $(g \ d) = d$ (source: Design Concepts in Programming Languages, p. 167). Make it simple: a fixed ...

View answer
Can String be a subtype of Character in a programming language?
4 votes

Subtyping is conceptually very different from inheritance. Subtyping refers to shared interfaces; $\tau$ is a subtype of $\tau'$, i.e. $\tau <: \tau'$, then all expressions of type $\tau$ could be ...

View answer
What does it mean that a let-binding can be treated polymorphically, only if its right-hand side is a syntactic value?
Accepted answer
3 votes

You seem to have been confounded by many related and similar but crucially different concepts! Let me attempt to explain them one at a time. Parametric polymorphism is the ability to write types that ...

View answer
The first Turing machine
3 votes

The TM only exists on paper. It is a theoretical model of computation. It actually can't be built (because the tape is infinitely long). So, the answer is: no, Turing never built a TM in real life, ...

View answer
Given a Turing machine M, is there a TM that computes the number of states M has?
Accepted answer
3 votes

I think you are a bit confused about TMs. A Turing machine, by canonical definition (as found in textbooks like [Sipser 1996], [Papadimitriou 1982] and [Hopcroft and Ullman 1979], as well as on ...

View answer
Introduction to type theory for a beginner?
3 votes

Why has no one proposed Benjamin Pierce's Types and Programming Languages? That is a good introduction to type theory. Bob (Robert) Harper's Practical Foundations of Programming Languages is also a ...

View answer
Beta reduction order in Lambda calulus
2 votes

No, you can try that and you'll get the same answer. Untyped lambda calculus has the Church-Rosser property, meaning that the order of $\beta$-reduction has no influence on the result of the reduction....

View answer
If it's Possible to Create the If-Statement from Simpler Primitives
2 votes

Contrary to what you (and many people) may think, in the field of programming languages, the most primitive control-flow operation is actually pattern matching! With a simple type system (say the ...

View answer
Symbolic Evaluation for Type Inference in a Dynamic Language
Accepted answer
2 votes

I am not sure you actually understand the terms you use here. Symbolic execution has nothing to do with type inference Symbolic execution is used for static analysis of programs, and is a special ...

View answer
Defining an HTML Template as an Algebraic Type
2 votes

You might also be interested in the Ur/Web programming language.

View answer
Are mathematical functions used in computer science?
0 votes

You can write mathematical functions in computer science. The OCaml function id (x: int): int = x, for example, is a mathematical function $id : \mathbb{Z} \rightarrow \mathbb{Z}$, where $id = n \...

View answer